Typeclasses for groups with an adjoined zero element #
This file provides just the typeclass definitions, and the projection lemmas that expose their members.
Main definitions #
@[instance]
@[class]
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 of this typeclass
- semigroup_with_zero.to_mul_zero_class
- mul_zero_one_class.to_mul_zero_class
- non_unital_non_assoc_semiring.to_mul_zero_class
- order_dual.mul_zero_class
- lex.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
- add_opposite.mul_zero_class
- ulift.mul_zero_class
- continuous_map.mul_zero_class
- filter.germ.mul_zero_class
- finsupp.mul_zero_class
- onote.mul_zero_class
- locally_constant.mul_zero_class
- zero_at_infty_continuous_map.mul_zero_class
Instances of other typeclasses for mul_zero_class
- mul_zero_class.has_sizeof_inst
@[instance]
@[class]
Predicate typeclass for expressing that a * b = 0 implies a = 0 or b = 0
for all a and b of type G₀.
Instances of this typeclass
- 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
- order_dual.no_zero_divisors
- lex.no_zero_divisors
- with_zero.no_zero_divisors
- with_top.no_zero_divisors
- with_bot.no_zero_divisors
- mul_opposite.no_zero_divisors
- add_opposite.no_zero_divisors
- set.no_zero_divisors
- subsemiring_class.no_zero_divisors
- subsemiring.no_zero_divisors
- subring.no_zero_divisors
- associates.no_zero_divisors
- ordinal.no_zero_divisors
- finset.no_zero_divisors
- set_semiring.no_zero_divisors
- ideal.no_zero_divisors
- subalgebra.no_zero_divisors
- polynomial.no_zero_divisors
- mv_polynomial.no_zero_divisors
- hahn_series.no_zero_divisors
- tropical.no_zero_divisors
- witt_vector.no_zero_divisors
@[class]
- 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 of this typeclass
- monoid_with_zero.to_semigroup_with_zero
- non_unital_semiring.to_semigroup_with_zero
- order_dual.semigroup_with_zero
- lex.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
- add_opposite.semigroup_with_zero
- continuous_map.semigroup_with_zero
- finsupp.semigroup_with_zero
- locally_constant.semigroup_with_zero
- zero_at_infty_continuous_map.semigroup_with_zero
Instances of other typeclasses for semigroup_with_zero
- semigroup_with_zero.has_sizeof_inst
@[instance]
@[instance]
@[class]
- 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 of this typeclass
- monoid_with_zero.to_mul_zero_one_class
- non_assoc_semiring.to_mul_zero_one_class
- order_dual.mul_zero_one_class
- lex.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
- add_opposite.mul_zero_one_class
- ulift.mul_zero_one_class
- locally_constant.mul_zero_one_class
Instances of other typeclasses for mul_zero_one_class
- mul_zero_one_class.has_sizeof_inst
@[instance]
@[instance]
@[instance]
@[instance]
@[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 of this typeclass
- 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
- order_dual.monoid_with_zero
- lex.monoid_with_zero
- with_zero.monoid_with_zero
- prod.monoid_with_zero
- non_unital_ring_hom.monoid_with_zero
- with_top.monoid_with_zero
- with_bot.monoid_with_zero
- pi.monoid_with_zero
- mul_opposite.monoid_with_zero
- add_opposite.monoid_with_zero
- ulift.monoid_with_zero
- ordinal.monoid_with_zero
- real.monoid_with_zero
- nonneg.monoid_with_zero
- continuous_linear_map.monoid_with_zero
- continuous_map.monoid_with_zero
- set.Icc.monoid_with_zero
- non_unital_star_alg_hom.monoid_with_zero
Instances of other typeclasses for monoid_with_zero
- monoid_with_zero.has_sizeof_inst
@[protected, instance]
Equations
- monoid_with_zero.to_semigroup_with_zero M₀ = {mul := monoid_with_zero.mul _inst_1, mul_assoc := _, zero := monoid_with_zero.zero _inst_1, zero_mul := _, mul_zero := _}
@[instance]
def
cancel_monoid_with_zero.to_monoid_with_zero
(M₀ : Type u_4)
[self : cancel_monoid_with_zero M₀] :
@[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₀), 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 of this typeclass
Instances of other typeclasses for cancel_monoid_with_zero
- cancel_monoid_with_zero.has_sizeof_inst
theorem
mul_left_cancel₀
{M₀ : Type u_1}
[cancel_monoid_with_zero M₀]
{a b c : M₀}
(ha : a ≠ 0)
(h : a * b = a * c) :
b = c
theorem
mul_right_cancel₀
{M₀ : Type u_1}
[cancel_monoid_with_zero M₀]
{a b c : M₀}
(hb : b ≠ 0)
(h : a * b = c * b) :
a = c
theorem
mul_left_injective₀
{M₀ : Type u_1}
[cancel_monoid_with_zero M₀]
{b : M₀}
(hb : b ≠ 0) :
function.injective (λ (a : M₀), a * b)
@[instance]
def
comm_monoid_with_zero.to_comm_monoid
(M₀ : Type u_4)
[self : comm_monoid_with_zero M₀] :
comm_monoid M₀
@[instance]
@[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₀), 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 of this typeclass
- 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
- order_dual.comm_monoid_with_zero
- lex.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
- ulift.comm_monoid_with_zero
- associates.comm_monoid_with_zero
- localization.comm_monoid_with_zero
- real.comm_monoid_with_zero
- nonneg.comm_monoid_with_zero
- nnreal.comm_monoid_with_zero
- continuous_map.comm_monoid_with_zero
- set.Icc.comm_monoid_with_zero
- ereal.comm_monoid_with_zero
Instances of other typeclasses for comm_monoid_with_zero
- comm_monoid_with_zero.has_sizeof_inst
@[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₀), 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 of this typeclass
- comm_group_with_zero.cancel_comm_monoid_with_zero
- is_domain.to_cancel_comm_monoid_with_zero
- order_dual.cancel_comm_monoid_with_zero
- lex.cancel_comm_monoid_with_zero
- nat.cancel_comm_monoid_with_zero
- associates.cancel_comm_monoid_with_zero
- punit.cancel_comm_monoid_with_zero
- set.Icc.cancel_comm_monoid_with_zero
- fractional_ideal.cancel_comm_monoid_with_zero
- ideal.cancel_comm_monoid_with_zero
Instances of other typeclasses for cancel_comm_monoid_with_zero
- cancel_comm_monoid_with_zero.has_sizeof_inst
@[instance]
def
cancel_comm_monoid_with_zero.to_comm_monoid_with_zero
(M₀ : Type u_4)
[self : cancel_comm_monoid_with_zero M₀] :
@[instance]
def
cancel_comm_monoid_with_zero.to_cancel_monoid_with_zero
(M₀ : Type u_4)
[self : cancel_comm_monoid_with_zero M₀] :
@[instance]
@[instance]
@[class]
- 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 of this typeclass
Instances of other typeclasses for group_with_zero
- group_with_zero.has_sizeof_inst
@[instance]
@[simp]
@[class]
- 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 of this typeclass
Instances of other typeclasses for comm_group_with_zero
- comm_group_with_zero.has_sizeof_inst
@[instance]
@[instance]
def
comm_group_with_zero.to_comm_monoid_with_zero
(G₀ : Type u_4)
[self : comm_group_with_zero G₀] :