# mathlibdocumentation

algebra.group_with_zero.defs

# 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 #

• group_with_zero
• comm_group_with_zero
@[instance]
def mul_zero_class.to_has_mul (M₀ : Type u_4) [self : mul_zero_class M₀] :
has_mul M₀
@[class]
structure mul_zero_class (M₀ : Type u_4) :
Type u_4
• 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 of this typeclass
Instances of other typeclasses for mul_zero_class
• mul_zero_class.has_sizeof_inst
@[instance]
def mul_zero_class.to_has_zero (M₀ : Type u_4) [self : mul_zero_class M₀] :
@[simp]
theorem zero_mul {M₀ : Type u_1} [mul_zero_class M₀] (a : M₀) :
0 * a = 0
@[simp]
theorem mul_zero {M₀ : Type u_1} [mul_zero_class M₀] (a : M₀) :
a * 0 = 0
@[class]
structure no_zero_divisors (M₀ : Type u_4) [has_mul M₀] [has_zero M₀] :
Prop
• eq_zero_or_eq_zero_of_mul_eq_zero : ∀ {a b : M₀}, a * b = 0a = 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 of this typeclass
@[class]
structure semigroup_with_zero (S₀ : Type u_4) :
Type u_4
• 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
Instances of other typeclasses for semigroup_with_zero
• semigroup_with_zero.has_sizeof_inst
@[instance]
def semigroup_with_zero.to_mul_zero_class (S₀ : Type u_4) [self : semigroup_with_zero S₀] :
@[instance]
def semigroup_with_zero.to_semigroup (S₀ : Type u_4) [self : semigroup_with_zero S₀] :
@[class]
structure mul_zero_one_class (M₀ : Type u_4) :
Type u_4
• 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
Instances of other typeclasses for mul_zero_one_class
• mul_zero_one_class.has_sizeof_inst
@[instance]
def mul_zero_one_class.to_mul_zero_class (M₀ : Type u_4) [self : mul_zero_one_class M₀] :
@[instance]
def mul_zero_one_class.to_mul_one_class (M₀ : Type u_4) [self : mul_zero_one_class M₀] :
@[instance]
def monoid_with_zero.to_mul_zero_one_class (M₀ : Type u_4) [self : monoid_with_zero M₀] :
@[instance]
def monoid_with_zero.to_monoid (M₀ : Type u_4) [self : monoid_with_zero M₀] :
monoid M₀
@[class]
structure monoid_with_zero (M₀ : Type u_4) :
Type u_4
• 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₀), = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : M₀), = 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
Instances of other typeclasses for monoid_with_zero
• monoid_with_zero.has_sizeof_inst
@[protected, instance]
Equations
@[instance]
@[class]
structure cancel_monoid_with_zero (M₀ : Type u_4) :
Type u_4
• 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₀), . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : M₀), . "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 0a * b = a * cb = c
• mul_right_cancel_of_ne_zero : ∀ {a b c : M₀}, b 0a * b = c * ba = 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} {a b c : M₀} (ha : a 0) (h : a * b = a * c) :
b = c
theorem mul_right_cancel₀ {M₀ : Type u_1} {a b c : M₀} (hb : b 0) (h : a * b = c * b) :
a = c
theorem mul_right_injective₀ {M₀ : Type u_1} {a : M₀} (ha : a 0) :
theorem mul_left_injective₀ {M₀ : Type u_1} {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₀] :
@[instance]
def comm_monoid_with_zero.to_monoid_with_zero (M₀ : Type u_4) [self : comm_monoid_with_zero M₀] :
@[class]
structure comm_monoid_with_zero (M₀ : Type u_4) :
Type u_4
• 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₀), . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : M₀), . "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
Instances of other typeclasses for comm_monoid_with_zero
• comm_monoid_with_zero.has_sizeof_inst
@[class]
structure cancel_comm_monoid_with_zero (M₀ : Type u_4) :
Type u_4
• 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₀), . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : M₀), . "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 0a * b = a * cb = c
• mul_right_cancel_of_ne_zero : ∀ {a b c : M₀}, b 0a * b = c * ba = 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
Instances of other typeclasses for cancel_comm_monoid_with_zero
• cancel_comm_monoid_with_zero.has_sizeof_inst
@[instance]
def group_with_zero.to_nontrivial (G₀ : Type u) [self : group_with_zero G₀] :
@[instance]
def group_with_zero.to_monoid_with_zero (G₀ : Type u) [self : group_with_zero G₀] :
@[class]
structure group_with_zero (G₀ : Type u) :
Type u
• 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₀), = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : G₀), = 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₀), = 1) . "try_refl_tac"
• zpow_succ' : (∀ (n : ) (a : G₀), = a * . "try_refl_tac"
• zpow_neg' : (∀ (n : ) (a : G₀), = a)⁻¹) . "try_refl_tac"
• exists_pair_ne : ∃ (x y : G₀), x y
• inv_zero : 0⁻¹ = 0
• mul_inv_cancel : ∀ (a : G₀), a 0a * 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]
def group_with_zero.to_div_inv_monoid (G₀ : Type u) [self : group_with_zero G₀] :
@[simp]
theorem inv_zero {G₀ : Type u} [group_with_zero G₀] :
0⁻¹ = 0
@[simp]
theorem mul_inv_cancel {G₀ : Type u} [group_with_zero G₀] {a : G₀} (h : a 0) :
a * a⁻¹ = 1
@[class]
structure comm_group_with_zero (G₀ : Type u_4) :
Type u_4
• 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₀), . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : G₀), . "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₀), . "try_refl_tac"
• zpow_succ' : (∀ (n : ) (a : G₀), = a * . "try_refl_tac"
• zpow_neg' : (∀ (n : ) (a : G₀), . "try_refl_tac"
• exists_pair_ne : ∃ (x y : G₀), x y
• inv_zero : 0⁻¹ = 0
• mul_inv_cancel : ∀ (a : G₀), a 0a * 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]
def comm_group_with_zero.to_group_with_zero (G₀ : Type u_4) [self : comm_group_with_zero G₀] :
@[instance]