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

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
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 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₀] :

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

    A mixin for cancellative multiplication by nonzero elements.

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

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

    Instances
    class MulDivCancelClass (M₀ : Type u_2) [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
    @[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₀ :

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

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