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 #

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

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

Instances
    @[simp]
    theorem MulZeroClass.zero_mul {M₀ : Type u} [self : MulZeroClass M₀] (a : M₀) :
    0 * a = 0

    Zero is a left absorbing element for multiplication

    @[simp]
    theorem MulZeroClass.mul_zero {M₀ : Type u} [self : MulZeroClass M₀] (a : M₀) :
    a * 0 = 0

    Zero is a right absorbing element for multiplication

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

    A mixin for left cancellative multiplication by nonzero elements.

    • mul_left_cancel_of_ne_zero : ∀ {a b c : M₀}, a 0a * b = a * cb = c

      Multiplication by a nonzero element is left cancellative.

    Instances
      theorem IsLeftCancelMulZero.mul_left_cancel_of_ne_zero {M₀ : Type u} [Mul M₀] [Zero M₀] [self : IsLeftCancelMulZero M₀] {a : M₀} {b : M₀} {c : M₀} :
      a 0a * b = a * cb = c

      Multiplication by a nonzero element is left cancellative.

      theorem mul_left_cancel₀ {M₀ : Type u_1} [Mul M₀] [Zero M₀] [IsLeftCancelMulZero 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₀] [IsLeftCancelMulZero M₀] {a : M₀} (ha : a 0) :
      Function.Injective fun (x : M₀) => a * x
      class IsRightCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀] :

      A mixin for right cancellative multiplication by nonzero elements.

      • mul_right_cancel_of_ne_zero : ∀ {a b c : M₀}, b 0a * b = c * ba = c

        Multiplicatin by a nonzero element is right cancellative.

      Instances
        theorem IsRightCancelMulZero.mul_right_cancel_of_ne_zero {M₀ : Type u} [Mul M₀] [Zero M₀] [self : IsRightCancelMulZero M₀] {a : M₀} {b : M₀} {c : M₀} :
        b 0a * b = c * ba = c

        Multiplicatin by a nonzero element is right cancellative.

        theorem mul_right_cancel₀ {M₀ : Type u_1} [Mul M₀] [Zero M₀] [IsRightCancelMulZero 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₀] [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 , IsRightCancelMulZero :

        A mixin for cancellative multiplication by nonzero elements.

          Instances
            class NoZeroDivisors (M₀ : Type u_4) [Mul M₀] [Zero M₀] :

            Predicate typeclass for expressing that a * b = 0 implies a = 0 or b = 0 for all a and b of type G₀.

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

            Instances
              theorem NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero {M₀ : Type u_4} [Mul M₀] [Zero M₀] [self : NoZeroDivisors M₀] {a : M₀} {b : M₀} :
              a * b = 0a = 0 b = 0

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

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

              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

                Zero is a left absorbing element for multiplication

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

                Zero is a right absorbing element for multiplication

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

                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

                  Zero is a left absorbing element for multiplication

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

                  Zero is a right absorbing element for multiplication

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

                  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

                    Zero is a left absorbing element for multiplication

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

                    Zero is a right absorbing element for multiplication

                  Instances
                    class CancelMonoidWithZero (M₀ : Type u_4) extends MonoidWithZero , IsCancelMulZero :
                    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 CommMonoid , Zero :
                        Type u_4

                        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

                          Zero is a left absorbing element for multiplication

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

                          Zero is a right absorbing element for multiplication

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

                          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
                              @[instance 100]
                              Equations
                              • CancelCommMonoidWithZero.toCancelMonoidWithZero = let __src := ; CancelMonoidWithZero.mk
                              class MulDivCancelClass (M₀ : Type u_4) [MonoidWithZero M₀] [Div M₀] :

                              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 0a * b / b = a
                              Instances
                                theorem MulDivCancelClass.mul_div_cancel {M₀ : Type u_4} [MonoidWithZero M₀] [Div M₀] [self : MulDivCancelClass M₀] (a : M₀) (b : M₀) :
                                b 0a * b / b = a
                                @[simp]
                                theorem mul_div_cancel_right₀ {M₀ : Type u_1} [MonoidWithZero M₀] [Div M₀] [MulDivCancelClass M₀] {b : M₀} (a : M₀) (hb : b 0) :
                                a * b / b = a
                                @[simp]
                                theorem mul_div_cancel_left₀ {M₀ : Type u_1} [CommMonoidWithZero M₀] [Div M₀] [MulDivCancelClass M₀] {a : M₀} (b : M₀) (ha : a 0) :
                                a * b / a = b
                                class GroupWithZero (G₀ : Type u) extends MonoidWithZero , Inv , Div , Nontrivial :

                                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⁻¹

                                  a / b := a * b⁻¹

                                • zpow : G₀G₀

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

                                • zpow_zero' : ∀ (a : G₀), GroupWithZero.zpow 0 a = 1

                                  a ^ 0 = 1

                                • zpow_succ' : ∀ (n : ) (a : G₀), GroupWithZero.zpow (Int.ofNat n.succ) a = GroupWithZero.zpow (Int.ofNat n) a * a

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

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

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

                                • 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 0a * a⁻¹ = 1

                                  Every nonzero element of a group with zero is invertible.

                                Instances
                                  @[simp]
                                  theorem GroupWithZero.inv_zero {G₀ : Type u} [self : GroupWithZero G₀] :
                                  0⁻¹ = 0

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

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

                                  Every nonzero element of a group with zero is invertible.

                                  @[simp]
                                  theorem mul_inv_cancel₀ {G₀ : Type u} [GroupWithZero G₀] {a : G₀} (h : a 0) :
                                  a * a⁻¹ = 1
                                  @[instance 100]
                                  Equations
                                  • =
                                  class CommGroupWithZero (G₀ : Type u_4) extends CommMonoidWithZero , Inv , Div , Nontrivial :
                                  Type u_4

                                  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⁻¹

                                    a / b := a * b⁻¹

                                  • zpow : G₀G₀

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

                                  • zpow_zero' : ∀ (a : G₀), CommGroupWithZero.zpow 0 a = 1

                                    a ^ 0 = 1

                                  • zpow_succ' : ∀ (n : ) (a : G₀), CommGroupWithZero.zpow (Int.ofNat n.succ) a = CommGroupWithZero.zpow (Int.ofNat n) a * a

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

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

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

                                  • 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 0a * a⁻¹ = 1

                                    Every nonzero element of a group with zero is invertible.

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

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

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

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

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

                                    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