• mul : M₀ → M₀ → M₀
• zero : M₀
• zero_mul : ∀ (a : M₀), 0 * a = 0
• mul_zero : ∀ (a : M₀), a * 0 = 0

Typeclass for expressing that a type M₀ with multiplication and a zero satisfies 0 * a = 0 and a * 0 = 0 for all a : M₀.

Instances

• semigroup_with_zero.to_mul_zero_class
• mul_zero_one_class.to_mul_zero_class
• non_unital_non_assoc_semiring.to_mul_zero_class
• with_zero.mul_zero_class
• prod.mul_zero_class
• with_top.mul_zero_class
• with_bot.mul_zero_class
• pi.mul_zero_class
• mul_opposite.mul_zero_class

• eq_zero_or_eq_zero_of_mul_eq_zero : ∀ {a b : M₀}, a * b = 0 → a = 0 ∨ b = 0

Predicate typeclass for expressing that a * b = 0 implies a = 0 or b = 0 for all a and b of type G₀.

Instances

• cancel_monoid_with_zero.to_no_zero_divisors
• group_with_zero.no_zero_divisors
• is_domain.to_no_zero_divisors
• canonically_ordered_comm_semiring.to_no_zero_divisors
• with_top.no_zero_divisors
• with_bot.no_zero_divisors
• mul_opposite.no_zero_divisors
• subsemiring.no_zero_divisors
• subring.no_zero_divisors
• associates.no_zero_divisors

• mul : S₀ → S₀ → S₀
• mul_assoc : ∀ (a b c : S₀), (a * b) * c = a * b * c
• zero : S₀
• zero_mul : ∀ (a : S₀), 0 * a = 0
• mul_zero : ∀ (a : S₀), a * 0 = 0

A type S₀ is a "semigroup with zero” if it is a semigroup with zero element, and 0 is left and right absorbing.

Instances

• monoid_with_zero.to_semigroup_with_zero
• non_unital_semiring.to_semigroup_with_zero
• with_zero.semigroup_with_zero
• prod.semigroup_with_zero
• with_top.semigroup_with_zero
• with_bot.semigroup_with_zero
• pi.semigroup_with_zero
• mul_opposite.semigroup_with_zero

• one : M₀
• mul : M₀ → M₀ → M₀
• one_mul : ∀ (a : M₀), 1 * a = a
• mul_one : ∀ (a : M₀), a * 1 = a
• zero : M₀
• zero_mul : ∀ (a : M₀), 0 * a = 0
• mul_zero : ∀ (a : M₀), a * 0 = 0

A typeclass for non-associative monoids with zero elements.

Instances

• monoid_with_zero.to_mul_zero_one_class
• non_assoc_semiring.to_mul_zero_one_class
• with_zero.mul_zero_one_class
• prod.mul_zero_one_class
• with_top.mul_zero_one_class
• with_bot.mul_zero_one_class
• pi.mul_zero_one_class
• mul_opposite.mul_zero_one_class

• mul : M₀ → M₀ → M₀
• mul_assoc : ∀ (a b c : M₀), (a * b) * c = a * b * c
• one : M₀
• one_mul : ∀ (a : M₀), 1 * a = a
• mul_one : ∀ (a : M₀), a * 1 = a
• npow : ℕ → M₀ → M₀
• npow_zero' : (∀ (x : M₀), monoid_with_zero.npow 0 x = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ℕ) (x : M₀), monoid_with_zero.npow n.succ x = x * monoid_with_zero.npow n x) . "try_refl_tac"
• zero : M₀
• zero_mul : ∀ (a : M₀), 0 * a = 0
• mul_zero : ∀ (a : M₀), a * 0 = 0

A type M₀ is a “monoid with zero” if it is a monoid with zero element, and 0 is left and right absorbing.

Instances

• cancel_monoid_with_zero.to_monoid_with_zero
• comm_monoid_with_zero.to_monoid_with_zero
• group_with_zero.to_monoid_with_zero
• semiring.to_monoid_with_zero
• with_zero.monoid_with_zero
• prod.monoid_with_zero
• with_top.monoid_with_zero
• with_bot.monoid_with_zero
• pi.monoid_with_zero
• mul_opposite.monoid_with_zero
• real.monoid_with_zero
• nonneg.monoid_with_zero

• mul : M₀ → M₀ → M₀
• mul_assoc : ∀ (a b c : M₀), (a * b) * c = a * b * c
• one : M₀
• one_mul : ∀ (a : M₀), 1 * a = a
• mul_one : ∀ (a : M₀), a * 1 = a
• npow : ℕ → M₀ → M₀
• npow_zero' : (∀ (x : M₀), cancel_monoid_with_zero.npow 0 x = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ℕ) (x : M₀), cancel_monoid_with_zero.npow n.succ x = x * cancel_monoid_with_zero.npow n x) . "try_refl_tac"
• zero : M₀
• zero_mul : ∀ (a : M₀), 0 * a = 0
• mul_zero : ∀ (a : M₀), a * 0 = 0
• mul_left_cancel_of_ne_zero : ∀ {a b c : M₀}, a ≠ 0 → a * b = a * c → b = c
• mul_right_cancel_of_ne_zero : ∀ {a b c : M₀}, b ≠ 0 → a * b = c * b → a = c

A type M is a cancel_monoid_with_zero if it is a monoid with zero element, 0 is left and right absorbing, and left/right multiplication by a non-zero element is injective.

Instances

• group_with_zero.cancel_monoid_with_zero
• cancel_comm_monoid_with_zero.to_cancel_monoid_with_zero
• is_domain.to_cancel_monoid_with_zero

• mul : M₀ → M₀ → M₀
• mul_assoc : ∀ (a b c : M₀), (a * b) * c = a * b * c
• one : M₀
• one_mul : ∀ (a : M₀), 1 * a = a
• mul_one : ∀ (a : M₀), a * 1 = a
• npow : ℕ → M₀ → M₀
• npow_zero' : (∀ (x : M₀), comm_monoid_with_zero.npow 0 x = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ℕ) (x : M₀), comm_monoid_with_zero.npow n.succ x = x * comm_monoid_with_zero.npow n x) . "try_refl_tac"
• mul_comm : ∀ (a b : M₀), a * b = b * a
• zero : M₀
• zero_mul : ∀ (a : M₀), 0 * a = 0
• mul_zero : ∀ (a : M₀), a * 0 = 0

A type M is a commutative “monoid with zero” if it is a commutative monoid with zero element, and 0 is left and right absorbing.

Instances

• cancel_comm_monoid_with_zero.to_comm_monoid_with_zero
• comm_group_with_zero.to_comm_monoid_with_zero
• comm_semiring.to_comm_monoid_with_zero
• linear_ordered_comm_monoid_with_zero.to_comm_monoid_with_zero
• with_zero.comm_monoid_with_zero
• prod.comm_monoid_with_zero
• with_top.comm_monoid_with_zero
• with_bot.comm_monoid_with_zero
• pi.comm_monoid_with_zero
• real.comm_monoid_with_zero
• associates.comm_monoid_with_zero
• nonneg.comm_monoid_with_zero
• nnreal.comm_monoid_with_zero

• mul : M₀ → M₀ → M₀
• mul_assoc : ∀ (a b c : M₀), (a * b) * c = a * b * c
• one : M₀
• one_mul : ∀ (a : M₀), 1 * a = a
• mul_one : ∀ (a : M₀), a * 1 = a
• npow : ℕ → M₀ → M₀
• npow_zero' : (∀ (x : M₀), cancel_comm_monoid_with_zero.npow 0 x = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ℕ) (x : M₀), cancel_comm_monoid_with_zero.npow n.succ x = x * cancel_comm_monoid_with_zero.npow n x) . "try_refl_tac"
• mul_comm : ∀ (a b : M₀), a * b = b * a
• zero : M₀
• zero_mul : ∀ (a : M₀), 0 * a = 0
• mul_zero : ∀ (a : M₀), a * 0 = 0
• mul_left_cancel_of_ne_zero : ∀ {a b c : M₀}, a ≠ 0 → a * b = a * c → b = c
• mul_right_cancel_of_ne_zero : ∀ {a b c : M₀}, b ≠ 0 → a * b = c * b → a = c

A type M is a cancel_comm_monoid_with_zero if it is a commutative monoid with zero element, 0 is left and right absorbing, and left/right multiplication by a non-zero element is injective.

Instances

• comm_group_with_zero.cancel_comm_monoid_with_zero
• is_domain.to_cancel_comm_monoid_with_zero
• nat.cancel_comm_monoid_with_zero
• associates.cancel_comm_monoid_with_zero
• punit.cancel_comm_monoid_with_zero

• mul : G₀ → G₀ → G₀
• mul_assoc : ∀ (a b c : G₀), (a * b) * c = a * b * c
• one : G₀
• one_mul : ∀ (a : G₀), 1 * a = a
• mul_one : ∀ (a : G₀), a * 1 = a
• npow : ℕ → G₀ → G₀
• npow_zero' : (∀ (x : G₀), group_with_zero.npow 0 x = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ℕ) (x : G₀), group_with_zero.npow n.succ x = x * group_with_zero.npow n x) . "try_refl_tac"
• zero : G₀
• zero_mul : ∀ (a : G₀), 0 * a = 0
• mul_zero : ∀ (a : G₀), a * 0 = 0
• inv : G₀ → G₀
• div : G₀ → G₀ → G₀
• div_eq_mul_inv : (∀ (a b : G₀), a / b = a * b⁻¹) . "try_refl_tac"
• zpow : ℤ → G₀ → G₀
• zpow_zero' : (∀ (a : G₀), group_with_zero.zpow 0 a = 1) . "try_refl_tac"
• zpow_succ' : (∀ (n : ℕ) (a : G₀), group_with_zero.zpow (int.of_nat n.succ) a = a * group_with_zero.zpow (int.of_nat n) a) . "try_refl_tac"
• zpow_neg' : (∀ (n : ℕ) (a : G₀), group_with_zero.zpow -[1+ n] a = (group_with_zero.zpow ↑(n.succ) a)⁻¹) . "try_refl_tac"
• exists_pair_ne : ∃ (x y : G₀), x ≠ y
• inv_zero : 0⁻¹ = 0
• mul_inv_cancel : ∀ (a : G₀), a ≠ 0 → a * a⁻¹ = 1

A type G₀ is a “group with zero” if it is a monoid with zero element (distinct from 1) such that every nonzero element is invertible. The type is required to come with an “inverse” function, and the inverse of 0 must be 0.

Examples include division rings and the ordered monoids that are the target of valuations in general valuation theory.

Instances

• comm_group_with_zero.to_group_with_zero
• division_ring.to_group_with_zero
• with_zero.group_with_zero
• mul_opposite.group_with_zero

• mul : G₀ → G₀ → G₀
• mul_assoc : ∀ (a b c : G₀), (a * b) * c = a * b * c
• one : G₀
• one_mul : ∀ (a : G₀), 1 * a = a
• mul_one : ∀ (a : G₀), a * 1 = a
• npow : ℕ → G₀ → G₀
• npow_zero' : (∀ (x : G₀), comm_group_with_zero.npow 0 x = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ℕ) (x : G₀), comm_group_with_zero.npow n.succ x = x * comm_group_with_zero.npow n x) . "try_refl_tac"
• mul_comm : ∀ (a b : G₀), a * b = b * a
• zero : G₀
• zero_mul : ∀ (a : G₀), 0 * a = 0
• mul_zero : ∀ (a : G₀), a * 0 = 0
• inv : G₀ → G₀
• div : G₀ → G₀ → G₀
• div_eq_mul_inv : (∀ (a b : G₀), a / b = a * b⁻¹) . "try_refl_tac"
• zpow : ℤ → G₀ → G₀
• zpow_zero' : (∀ (a : G₀), comm_group_with_zero.zpow 0 a = 1) . "try_refl_tac"
• zpow_succ' : (∀ (n : ℕ) (a : G₀), comm_group_with_zero.zpow (int.of_nat n.succ) a = a * comm_group_with_zero.zpow (int.of_nat n) a) . "try_refl_tac"
• zpow_neg' : (∀ (n : ℕ) (a : G₀), comm_group_with_zero.zpow -[1+ n] a = (comm_group_with_zero.zpow ↑(n.succ) a)⁻¹) . "try_refl_tac"
• exists_pair_ne : ∃ (x y : G₀), x ≠ y
• inv_zero : 0⁻¹ = 0
• mul_inv_cancel : ∀ (a : G₀), a ≠ 0 → a * a⁻¹ = 1

A type G₀ is a commutative “group with zero” if it is a commutative monoid with zero element (distinct from 1) such that every nonzero element is invertible. The type is required to come with an “inverse” function, and the inverse of 0 must be 0.

Instances

• field.to_comm_group_with_zero
• linear_ordered_comm_group_with_zero.to_comm_group_with_zero
• with_zero.comm_group_with_zero