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₀, Zero M₀ : Type u

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

• 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

class IsLeftCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀] : Prop

A mixin for left cancellative multiplication by nonzero elements.

• mul_left_cancel_of_ne_zero {a : M₀} : a ≠ 0 → IsLeftRegular a

  Multiplication by a nonzero element is left cancellative.

theorem isLeftCancelMulZero_iff (M₀ : Type u) [Mul M₀] [Zero M₀] : IsLeftCancelMulZero M₀ ↔ ∀ {a : M₀}, a ≠ 0 → IsLeftRegular a

theorem mul_left_cancel₀ {M₀ : Type u_1} [Mul M₀] [Zero M₀] [IsLeftCancelMulZero M₀] {a b c : M₀} (ha : a ≠ 0) (h : a * b = a * c) : b = c

theorem mul_right_injective₀ {M₀ : Type u_1} [Mul M₀] [Zero M₀] [IsLeftCancelMulZero M₀] {a : M₀} (ha : a ≠ 0) : Function.Injective fun (x : M₀) => a * x

class IsRightCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀] : Prop

A mixin for right cancellative multiplication by nonzero elements.

• mul_right_cancel_of_ne_zero {a : M₀} : a ≠ 0 → IsRightRegular a

  Multiplication by a nonzero element is right cancellative.

theorem isRightCancelMulZero_iff (M₀ : Type u) [Mul M₀] [Zero M₀] : IsRightCancelMulZero M₀ ↔ ∀ {a : M₀}, a ≠ 0 → IsRightRegular a

theorem mul_right_cancel₀ {M₀ : Type u_1} [Mul M₀] [Zero M₀] [IsRightCancelMulZero M₀] {a b c : M₀} (hb : b ≠ 0) (h : a * b = c * b) : a = c

theorem mul_left_injective₀ {M₀ : Type u_1} [Mul M₀] [Zero M₀] [IsRightCancelMulZero M₀] {b : M₀} (hb : b ≠ 0) : Function.Injective fun (a : M₀) => a * b

class IsCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀] extends IsLeftCancelMulZero M₀, IsRightCancelMulZero M₀ : Prop

A mixin for cancellative multiplication by nonzero elements.

• mul_left_cancel_of_ne_zero {a : M₀} : a ≠ 0 → IsLeftRegular a
• mul_right_cancel_of_ne_zero {a : M₀} : a ≠ 0 → IsRightRegular a

theorem isCancelMulZero_iff (M₀ : Type u) [Mul M₀] [Zero M₀] : IsCancelMulZero M₀ ↔ IsLeftCancelMulZero M₀ ∧ IsRightCancelMulZero M₀

theorem isCancelMulZero_iff_forall_isRegular {M₀ : Type u_2} [Mul M₀] [Zero M₀] : IsCancelMulZero M₀ ↔ ∀ {a : M₀}, a ≠ 0 → IsRegular a

class NoZeroDivisors (M₀ : Type u_2) [Mul M₀] [Zero M₀] : Prop

Predicate typeclass for expressing that a * b = 0 implies a = 0 or b = 0 for all a and b of type M₀. It is weaker than IsCancelMulZero in general, but equivalent to it if M₀ is a (not necessarily unital or associative) ring.

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

  For all a and b of M₀, a * b = 0 implies a = 0 or b = 0.

theorem noZeroDivisors_iff (M₀ : Type u_2) [Mul M₀] [Zero M₀] : NoZeroDivisors M₀ ↔ ∀ {a b : M₀}, a * b = 0 → a = 0 ∨ b = 0

class SemigroupWithZero (S₀ : Type u) extends Semigroup S₀, MulZeroClass S₀ : Type u

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

• 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

class MulZeroOneClass (M₀ : Type u) extends MulOneClass M₀, MulZeroClass M₀ : Type u

A typeclass for non-associative monoids with zero elements.

• 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

class MonoidWithZero (M₀ : Type u) extends Monoid M₀, MulZeroOneClass M₀, SemigroupWithZero M₀ : Type u

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

• 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.npow 0 x = 1
• npow_succ (n : ℕ) (x : M₀) : Monoid.npow (n + 1) x = Monoid.npow n x * x
• zero : M₀
• zero_mul (a : M₀) : 0 * a = 0
• mul_zero (a : M₀) : a * 0 = 0

theorem pow_mul_apply_eq_pow_mul {M₀ : Type u_1} [MonoidWithZero M₀] {M : Type u_2} [Monoid M] (f : M₀ → M) {x : M₀} (hx : ∀ (y : M₀), f (x * y) = f x * f y) (n : ℕ) (y : M₀) : f (x ^ n * y) = f x ^ n * f y

If x is multiplicative with respect to f, then so is any x^n.

class CancelMonoidWithZero (M₀ : Type u_2) extends MonoidWithZero M₀, IsCancelMulZero M₀ : Type u_2

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.

• 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.npow 0 x = 1
• npow_succ (n : ℕ) (x : M₀) : Monoid.npow (n + 1) x = Monoid.npow n x * x
• zero : M₀
• zero_mul (a : M₀) : 0 * a = 0
• mul_zero (a : M₀) : a * 0 = 0
• mul_left_cancel_of_ne_zero {a : M₀} : a ≠ 0 → IsLeftRegular a
• mul_right_cancel_of_ne_zero {a : M₀} : a ≠ 0 → IsRightRegular a

class CommMonoidWithZero (M₀ : Type u_2) extends CommMonoid M₀, MonoidWithZero M₀ : Type u_2

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.

• 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.npow 0 x = 1
• npow_succ (n : ℕ) (x : M₀) : Monoid.npow (n + 1) x = Monoid.npow n x * x
• 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

theorem mul_left_inj' {M₀ : Type u_1} [CancelMonoidWithZero M₀] {a b c : M₀} (hc : c ≠ 0) : a * c = b * c ↔ a = b

theorem mul_right_inj' {M₀ : Type u_1} [CancelMonoidWithZero M₀] {a b c : M₀} (ha : a ≠ 0) : a * b = a * c ↔ b = c

theorem IsLeftCancelMulZero.to_isRightCancelMulZero {M₀ : Type u_1} [CommSemigroup M₀] [Zero M₀] [IsLeftCancelMulZero M₀] : IsRightCancelMulZero M₀

theorem IsRightCancelMulZero.to_isLeftCancelMulZero {M₀ : Type u_1} [CommSemigroup M₀] [Zero M₀] [IsRightCancelMulZero M₀] : IsLeftCancelMulZero M₀

theorem IsLeftCancelMulZero.to_isCancelMulZero {M₀ : Type u_1} [CommSemigroup M₀] [Zero M₀] [IsLeftCancelMulZero M₀] : IsCancelMulZero M₀

theorem IsRightCancelMulZero.to_isCancelMulZero {M₀ : Type u_1} [CommSemigroup M₀] [Zero M₀] [IsRightCancelMulZero M₀] : IsCancelMulZero M₀

class CancelCommMonoidWithZero (M₀ : Type u_2) extends CommMonoidWithZero M₀, IsLeftCancelMulZero M₀ : Type u_2

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.

• 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.npow 0 x = 1
• npow_succ (n : ℕ) (x : M₀) : Monoid.npow (n + 1) x = Monoid.npow n x * x
• 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 : M₀} : a ≠ 0 → IsLeftRegular a

@[instance 100]

instance CancelCommMonoidWithZero.toCancelMonoidWithZero {M₀ : Type u_1} [CancelCommMonoidWithZero M₀] : CancelMonoidWithZero M₀

Equations

• CancelCommMonoidWithZero.toCancelMonoidWithZero = { toMonoidWithZero := inst✝.toMonoidWithZero, toIsCancelMulZero := ⋯ }

class MulDivCancelClass (M₀ : Type u_2) [MonoidWithZero M₀] [Div M₀] : Prop

Prop-valued mixin for a monoid with zero to be equipped with a cancelling division.

The obvious use case is groups with zero, but this condition is also satisfied by ℕ, ℤ and, more generally, any Euclidean domain.

• mul_div_cancel (a b : M₀) : b ≠ 0 → a * b / b = a

@[simp]

theorem mul_div_cancel_right₀ {M₀ : Type u_1} [MonoidWithZero M₀] [Div M₀] [MulDivCancelClass M₀] (a : M₀) {b : M₀} (hb : b ≠ 0) : a * b / b = a

@[simp]

theorem mul_div_cancel_left₀ {M₀ : Type u_1} [CommMonoidWithZero M₀] [Div M₀] [MulDivCancelClass M₀] (b : M₀) {a : M₀} (ha : a ≠ 0) : a * b / a = b

class GroupWithZero (G₀ : Type u) extends MonoidWithZero G₀, DivInvMonoid G₀, Nontrivial G₀ : Type u

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.

• 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₀) : Monoid.npow 0 x = 1
• npow_succ (n : ℕ) (x : G₀) : Monoid.npow (n + 1) x = Monoid.npow n 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⁻¹
• zpow : ℤ → G₀ → G₀
• zpow_zero' (a : G₀) : GroupWithZero.zpow 0 a = 1
• zpow_succ' (n : ℕ) (a : G₀) : GroupWithZero.zpow (↑n.succ) a = GroupWithZero.zpow (↑n) a * a
• zpow_neg' (n : ℕ) (a : G₀) : GroupWithZero.zpow (Int.negSucc n) a = (GroupWithZero.zpow (↑n.succ) a)⁻¹
• exists_pair_ne : ∃ (x : G₀), ∃ (y : G₀), x ≠ y
• inv_zero : 0⁻¹ = 0

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

• mul_inv_cancel (a : G₀) : a ≠ 0 → a * a⁻¹ = 1

  Every nonzero element of a group with zero is invertible.

@[simp]

theorem inv_zero {G₀ : Type u} [GroupWithZero G₀] : 0⁻¹ = 0

@[simp]

theorem mul_inv_cancel₀ {G₀ : Type u} [GroupWithZero G₀] {a : G₀} (h : a ≠ 0) : a * a⁻¹ = 1

@[instance 100]

instance GroupWithZero.toMulDivCancelClass {G₀ : Type u} [GroupWithZero G₀] : MulDivCancelClass G₀

class CommGroupWithZero (G₀ : Type u_2) extends CommMonoidWithZero G₀, GroupWithZero G₀ : Type u_2

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.

• 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₀) : Monoid.npow 0 x = 1
• npow_succ (n : ℕ) (x : G₀) : Monoid.npow (n + 1) x = Monoid.npow n 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⁻¹
• zpow : ℤ → G₀ → G₀
• zpow_zero' (a : G₀) : CommGroupWithZero.zpow 0 a = 1
• zpow_succ' (n : ℕ) (a : G₀) : CommGroupWithZero.zpow (↑n.succ) a = CommGroupWithZero.zpow (↑n) a * a
• zpow_neg' (n : ℕ) (a : G₀) : CommGroupWithZero.zpow (Int.negSucc n) a = (CommGroupWithZero.zpow (↑n.succ) a)⁻¹
• exists_pair_ne : ∃ (x : G₀), ∃ (y : G₀), x ≠ y
• inv_zero : 0⁻¹ = 0
• mul_inv_cancel (a : G₀) : a ≠ 0 → a * a⁻¹ = 1

theorem eq_zero_or_one_of_sq_eq_self {M₀ : Type u_1} [CancelMonoidWithZero M₀] {x : M₀} (hx : x ^ 2 = x) : x = 0 ∨ x = 1

@[simp]

theorem mul_inv_cancel_right₀ {G₀ : Type u} [GroupWithZero G₀] {b : G₀} (h : b ≠ 0) (a : G₀) : a * b * b⁻¹ = a

@[simp]

theorem mul_inv_cancel_left₀ {G₀ : Type u} [GroupWithZero G₀] {a : G₀} (h : a ≠ 0) (b : G₀) : a * (a⁻¹ * b) = b

theorem mul_eq_zero_of_left {M₀ : Type u_1} [MulZeroClass M₀] {a : M₀} (h : a = 0) (b : M₀) : a * b = 0

theorem mul_eq_zero_of_right {M₀ : Type u_1} [MulZeroClass M₀] (a : M₀) {b : M₀} (h : b = 0) : a * b = 0

theorem noZeroDivisors_iff_right_eq_zero_of_mul {M₀ : Type u_1} [MulZeroClass M₀] : NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → ∀ (y : M₀), x * y = 0 → y = 0

theorem noZeroDivisors_iff_left_eq_zero_of_mul {M₀ : Type u_1} [MulZeroClass M₀] : NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → ∀ (y : M₀), y * x = 0 → y = 0

theorem noZeroDivisors_iff_eq_zero_of_mul {M₀ : Type u_1} [MulZeroClass M₀] : NoZeroDivisors M₀ ↔ ∀ (x : M₀), x ≠ 0 → (∀ (y : M₀), x * y = 0 → y = 0) ∧ ∀ (y : M₀), y * x = 0 → y = 0

@[simp]

theorem mul_eq_zero {M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a 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} [MulZeroClass M₀] [NoZeroDivisors M₀] {a 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} [MulZeroClass M₀] [NoZeroDivisors M₀] {a 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} [MulZeroClass M₀] [NoZeroDivisors M₀] {a 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} [MulZeroClass M₀] [NoZeroDivisors M₀] {a 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} [MulZeroClass M₀] [NoZeroDivisors M₀] {a : M₀} : a * a = 0 ↔ a = 0

theorem zero_eq_mul_self {M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a : M₀} : 0 = a * a ↔ a = 0

theorem mul_self_ne_zero {M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a : M₀} : a * a ≠ 0 ↔ a ≠ 0

theorem zero_ne_mul_self {M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a : M₀} : 0 ≠ a * a ↔ a ≠ 0

theorem mul_eq_zero_iff_left {M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀} (ha : a ≠ 0) : a * b = 0 ↔ b = 0

theorem mul_eq_zero_iff_right {M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀} (hb : b ≠ 0) : a * b = 0 ↔ a = 0

theorem mul_ne_zero_iff_left {M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀} (ha : a ≠ 0) : a * b ≠ 0 ↔ b ≠ 0

theorem mul_ne_zero_iff_right {M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀} (hb : b ≠ 0) : a * b ≠ 0 ↔ a ≠ 0