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

ink

theorem eq_of_sub_eq_zero' {R : Type u_1} [inst : AddGroup R] {a : R} {b : R} (h : a - b = 0) : a = b

ink

theorem pow_succ'' {M : Type u_1} [inst : Monoid M] (n : ℕ) (a : M) : a ^ Nat.succ n = a * a ^ n

ink

class MulZeroClass (M₀ : Type u) extends Mul , Zero : Type u

• Zero is a left absorbing element for multiplication

  zero_mul : ∀ (a : M₀), 0 * a = 0

• Zero is a right absorbing element for multiplication

  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₀.

ink

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

• Multiplicatin by a nonzero element is left cancellative.

  mul_left_cancel_of_ne_zero : ∀ {a b c : M₀}, a ≠ 0 → a * b = a * c → b = c

A mixin for left cancellative multiplication by nonzero elements.

ink

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

ink

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

ink

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

• Multiplicatin by a nonzero element is right cancellative.

  mul_right_cancel_of_ne_zero : ∀ {a b c : M₀}, b ≠ 0 → a * b = c * b → a = c

A mixin for right cancellative multiplication by nonzero elements.

ink

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

ink

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

ink

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

A mixin for cancellative multiplication by nonzero elements.

ink

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

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

  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₀.

ink

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

• Zero is a left absorbing element for multiplication

  zero_mul : ∀ (a : S₀), 0 * a = 0

• Zero is a right absorbing element for multiplication

  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.

ink

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

• Zero is a left absorbing element for multiplication

  zero_mul : ∀ (a : M₀), 0 * a = 0

• Zero is a right absorbing element for multiplication

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

A typeclass for non-associative monoids with zero elements.

ink

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

• Zero is a left absorbing element for multiplication

  zero_mul : ∀ (a : M₀), 0 * a = 0

• Zero is a right absorbing element for multiplication

  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.

ink

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

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.

ink

class CommMonoidWithZero (M₀ : Type u_1) extends CommMonoid , Zero : Type u_1

• Zero is a left absorbing element for multiplication

  zero_mul : ∀ (a : M₀), 0 * a = 0

• Zero is a right absorbing element for multiplication

  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.

ink

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

ink

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

ink

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

ink

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

ink

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

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.

ink

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

Equations

• CancelCommMonoidWithZero.toCancelMonoidWithZero = let src := (_ : IsCancelMulZero M₀); CancelMonoidWithZero.mk

ink

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

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

  zpow : ℤ → G₀ → G₀

• a ^ 0 = 1

  zpow_zero' : autoParam (∀ (a : G₀), zpow 0 a = 1) _auto✝

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

  zpow_succ' : autoParam (∀ (n : ℕ) (a : G₀), zpow (Int.ofNat (Nat.succ n)) a = a * zpow (Int.ofNat n) a) _auto✝

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

  zpow_neg' : autoParam (∀ (n : ℕ) (a : G₀), zpow (Int.negSucc n) a = (zpow (↑(Nat.succ n)) a)⁻¹) _auto✝
• toNontrivial : Nontrivial G₀

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

  inv_zero : 0⁻¹ = 0

• Every nonzero element of a group with zero is invertible.

  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.

ink

@[simp]

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

ink

class CommGroupWithZero (G₀ : Type u_1) extends CommMonoidWithZero , Inv , Div , Nontrivial : Type u_1

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

  zpow : ℤ → G₀ → G₀

• a ^ 0 = 1

  zpow_zero' : autoParam (∀ (a : G₀), zpow 0 a = 1) _auto✝

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

  zpow_succ' : autoParam (∀ (n : ℕ) (a : G₀), zpow (Int.ofNat (Nat.succ n)) a = a * zpow (Int.ofNat n) a) _auto✝

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

  zpow_neg' : autoParam (∀ (n : ℕ) (a : G₀), zpow (Int.negSucc n) a = (zpow (↑(Nat.succ n)) a)⁻¹) _auto✝
• toNontrivial : Nontrivial G₀

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

  inv_zero : 0⁻¹ = 0

• Every nonzero element of a group with zero is invertible.

  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.

ink

instance NeZero.one (M₀ : Type u_1) [inst : MulZeroOneClass M₀] [inst : Nontrivial M₀] : NeZero 1

In a nontrivial monoid with zero, zero and one are different.

Equations

• NeZero.one = NeZero.one.proof_1

ink

theorem pullback_nonzero {M₀ : Type u_2} {M₀' : Type u_1} [inst : MulZeroOneClass M₀] [inst : Nontrivial M₀] [inst : Zero M₀'] [inst : One M₀'] (f : M₀' → M₀) (zero : f 0 = 0) (one : f 1 = 1) : Nontrivial M₀'

Pullback a nontrivial instance along a function sending 0 to 0 and 1 to 1.

ink

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

ink

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

ink

@[simp]

theorem mul_eq_zero {M₀ : Type u_1} [inst : MulZeroClass M₀] [inst : NoZeroDivisors M₀] {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.

ink

@[simp]

theorem zero_eq_mul {M₀ : Type u_1} [inst : MulZeroClass M₀] [inst : NoZeroDivisors M₀] {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.

ink

theorem mul_ne_zero_iff {M₀ : Type u_1} [inst : MulZeroClass M₀] [inst : NoZeroDivisors M₀] {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.

ink

theorem mul_eq_zero_comm {M₀ : Type u_1} [inst : MulZeroClass M₀] [inst : NoZeroDivisors M₀] {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.

ink

theorem mul_ne_zero_comm {M₀ : Type u_1} [inst : MulZeroClass M₀] [inst : NoZeroDivisors M₀] {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.

ink

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

ink

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

ink

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

ink

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