# Documentation

Mathlib.Algebra.GroupWithZero.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 #

• GroupWithZero
• CommGroupWithZero
class MulZeroClass (M₀ : Type u) extends , :
• mul : M₀M₀M₀
• zero : M₀
• zero_mul : ∀ (a : M₀), 0 * a = 0

Zero is a left absorbing element for multiplication

• mul_zero : ∀ (a : M₀), a * 0 = 0

Zero is a right absorbing element for multiplication

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
class IsLeftCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀] :
• mul_left_cancel_of_ne_zero : ∀ {a b c : M₀}, a 0a * b = a * cb = c

Multiplication by a nonzero element is left cancellative.

A mixin for left cancellative multiplication by nonzero elements.

Instances
theorem mul_left_cancel₀ {M₀ : Type u_1} [Mul M₀] [Zero M₀] [] {a : M₀} {b : M₀} {c : M₀} (ha : a 0) (h : a * b = a * c) :
b = c
theorem mul_right_injective₀ {M₀ : Type u_1} [Mul M₀] [Zero M₀] [] {a : M₀} (ha : a 0) :
Function.Injective ((fun x x_1 => x * x_1) a)
class IsRightCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀] :
• mul_right_cancel_of_ne_zero : ∀ {a b c : M₀}, b 0a * b = c * ba = c

Multiplicatin by a nonzero element is right cancellative.

A mixin for right cancellative multiplication by nonzero elements.

Instances
theorem mul_right_cancel₀ {M₀ : Type u_1} [Mul M₀] [Zero M₀] [] {a : M₀} {b : M₀} {c : M₀} (hb : b 0) (h : a * b = c * b) :
a = c
theorem mul_left_injective₀ {M₀ : Type u_1} [Mul M₀] [Zero M₀] [] {b : M₀} (hb : b 0) :
Function.Injective fun a => a * b
class IsCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀] extends , :

A mixin for cancellative multiplication by nonzero elements.

Instances
class NoZeroDivisors (M₀ : Type u_4) [Mul M₀] [Zero M₀] :
• eq_zero_or_eq_zero_of_mul_eq_zero : ∀ {a b : M₀}, a * b = 0a = 0 b = 0

For all a and b of G₀, a * b = 0 implies a = 0 or 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
class SemigroupWithZero (S₀ : Type u) extends , :
• 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

Zero is a left absorbing element for multiplication

• mul_zero : ∀ (a : S₀), a * 0 = 0

Zero is a right absorbing element for multiplication

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

Instances
class MulZeroOneClass (M₀ : Type u) extends , :
• 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

Zero is a left absorbing element for multiplication

• mul_zero : ∀ (a : M₀), a * 0 = 0

Zero is a right absorbing element for multiplication

A typeclass for non-associative monoids with zero elements.

Instances
class MonoidWithZero (M₀ : Type u) extends , :
• 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
• npow_succ : ∀ (n : ) (x : M₀), Monoid.npow (n + 1) x = x *
• zero : M₀
• zero_mul : ∀ (a : M₀), 0 * a = 0

Zero is a left absorbing element for multiplication

• mul_zero : ∀ (a : M₀), a * 0 = 0

Zero is a right absorbing element for multiplication

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

Instances
class CancelMonoidWithZero (M₀ : Type u_4) extends , :
Type u_4

A type M is a CancelMonoidWithZero 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
class CommMonoidWithZero (M₀ : Type u_4) extends , :
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
• npow_succ : ∀ (n : ) (x : M₀), Monoid.npow (n + 1) x = x *
• mul_comm : ∀ (a b : M₀), a * b = b * a
• zero : M₀
• zero_mul : ∀ (a : M₀), 0 * a = 0

Zero is a left absorbing element for multiplication

• mul_zero : ∀ (a : M₀), a * 0 = 0

Zero is a right absorbing element for multiplication

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
theorem mul_left_inj' {M₀ : Type u_1} [] {a : M₀} {b : M₀} {c : M₀} (hc : c 0) :
a * c = b * c a = b
theorem mul_right_inj' {M₀ : Type u_1} [] {a : M₀} {b : M₀} {c : M₀} (ha : a 0) :
a * b = a * c b = c
theorem IsLeftCancelMulZero.to_isRightCancelMulZero {M₀ : Type u_1} [] [Zero M₀] [] :
theorem IsRightCancelMulZero.to_isLeftCancelMulZero {M₀ : Type u_1} [] [Zero M₀] [] :
theorem IsLeftCancelMulZero.to_isCancelMulZero {M₀ : Type u_1} [] [Zero M₀] [] :
theorem IsRightCancelMulZero.to_isCancelMulZero {M₀ : Type u_1} [] [Zero M₀] [] :
class CancelCommMonoidWithZero (M₀ : Type u_4) extends , :
Type u_4

A type M is a CancelCommMonoidWithZero 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
class GroupWithZero (G₀ : Type u) extends , , , :
• 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
• npow_succ : ∀ (n : ) (x : G₀), Monoid.npow (n + 1) x = x *
• 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⁻¹

a / b := a * b⁻¹

• zpow : G₀G₀

The power operation: a ^ n = a * ··· * a; a ^ (-n) = a⁻¹ * ··· a⁻¹ (n times)

• zpow_zero' : ∀ (a : G₀), = 1

a ^ 0 = 1

• zpow_succ' : ∀ (n : ) (a : G₀), = a *

a ^ (n + 1) = a * a ^ n

• zpow_neg' : ∀ (n : ) (a : G₀), = (GroupWithZero.zpow (↑()) a)⁻¹

a ^ -(n + 1) = (a ^ (n + 1))⁻¹

• exists_pair_ne : x y, x y
• inv_zero : 0⁻¹ = 0

The inverse of 0 in a group with zero is 0.

• mul_inv_cancel : ∀ (a : G₀), a 0a * a⁻¹ = 1

Every nonzero element of a group with zero is invertible.

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
@[simp]
theorem mul_inv_cancel {G₀ : Type u} [] {a : G₀} (h : a 0) :
a * a⁻¹ = 1
class CommGroupWithZero (G₀ : Type u_4) extends , , , :
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₀), = 1
• npow_succ : ∀ (n : ) (x : G₀), Monoid.npow (n + 1) x = x *
• 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⁻¹

a / b := a * b⁻¹

• zpow : G₀G₀

The power operation: a ^ n = a * ··· * a; a ^ (-n) = a⁻¹ * ··· a⁻¹ (n times)

• zpow_zero' : ∀ (a : G₀),

a ^ 0 = 1

• zpow_succ' : ∀ (n : ) (a : G₀), = a *

a ^ (n + 1) = a * a ^ n

• zpow_neg' : ∀ (n : ) (a : G₀), = (CommGroupWithZero.zpow (↑()) a)⁻¹

a ^ -(n + 1) = (a ^ (n + 1))⁻¹

• exists_pair_ne : x y, x y
• inv_zero : 0⁻¹ = 0

The inverse of 0 in a group with zero is 0.

• mul_inv_cancel : ∀ (a : G₀), a 0a * a⁻¹ = 1

Every nonzero element of a group with zero is invertible.

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
@[simp]
theorem mul_inv_cancel_right₀ {G₀ : Type u} [] {b : G₀} (h : b 0) (a : G₀) :
a * b * b⁻¹ = a
@[simp]
theorem mul_inv_cancel_left₀ {G₀ : Type u} [] {a : G₀} (h : a 0) (b : G₀) :
a * (a⁻¹ * b) = b
theorem mul_eq_zero_of_left {M₀ : Type u_1} [] {a : M₀} (h : a = 0) (b : M₀) :
a * b = 0
theorem mul_eq_zero_of_right {M₀ : Type u_1} [] (a : M₀) {b : M₀} (h : b = 0) :
a * b = 0
@[simp]
theorem mul_eq_zero {M₀ : Type u_1} [] [] {a : M₀} {b : M₀} :
a * b = 0 a = 0 b = 0

If α has no zero divisors, then the product of two elements equals zero iff one of them equals zero.

@[simp]
theorem zero_eq_mul {M₀ : Type u_1} [] [] {a : M₀} {b : M₀} :
0 = a * b a = 0 b = 0

If α has no zero divisors, then the product of two elements equals zero iff one of them equals zero.

theorem mul_ne_zero_iff {M₀ : Type u_1} [] [] {a : M₀} {b : M₀} :
a * b 0 a 0 b 0

If α has no zero divisors, then the product of two elements is nonzero iff both of them are nonzero.

theorem mul_eq_zero_comm {M₀ : Type u_1} [] [] {a : M₀} {b : M₀} :
a * b = 0 b * a = 0

If α has no zero divisors, then for elements a, b : α, a * b equals zero iff so is b * a.

theorem mul_ne_zero_comm {M₀ : Type u_1} [] [] {a : M₀} {b : M₀} :
a * b 0 b * a 0

If α has no zero divisors, then for elements a, b : α, a * b is nonzero iff so is b * a.

theorem mul_self_eq_zero {M₀ : Type u_1} [] [] {a : M₀} :
a * a = 0 a = 0
theorem zero_eq_mul_self {M₀ : Type u_1} [] [] {a : M₀} :
0 = a * a a = 0
theorem mul_self_ne_zero {M₀ : Type u_1} [] [] {a : M₀} :
a * a 0 a 0
theorem zero_ne_mul_self {M₀ : Type u_1} [] [] {a : M₀} :
0 a * a a 0