# Documentation

Mathlib.Algebra.GroupWithZero.Basic

# Groups with an adjoined zero element #

This file describes structures that are not usually studied on their own right in mathematics, namely a special sort of monoid: apart from a distinguished “zero element” they form a group, or in other words, they are groups with an adjoined zero element.

Examples are:

• division rings;
• the value monoid of a multiplicative valuation;
• in particular, the non-negative real numbers.

## Main definitions #

Various lemmas about GroupWithZero and CommGroupWithZero. To reduce import dependencies, the type-classes themselves are in Algebra.GroupWithZero.Defs.

## Implementation details #

As is usual in mathlib, we extend the inverse function to the zero element, and require 0⁻¹ = 0.

theorem left_ne_zero_of_mul {M₀ : Type u_1} [inst : ] {a : M₀} {b : M₀} :
a * b 0a 0
theorem right_ne_zero_of_mul {M₀ : Type u_1} [inst : ] {a : M₀} {b : M₀} :
a * b 0b 0
theorem ne_zero_and_ne_zero_of_mul {M₀ : Type u_1} [inst : ] {a : M₀} {b : M₀} (h : a * b 0) :
a 0 b 0
theorem mul_eq_zero_of_ne_zero_imp_eq_zero {M₀ : Type u_1} [inst : ] {a : M₀} {b : M₀} (h : a 0b = 0) :
a * b = 0
theorem zero_mul_eq_const {M₀ : Type u_1} [inst : ] :
(fun x x_1 => x * x_1) 0 =

To match one_mul_eq_id.

theorem mul_zero_eq_const {M₀ : Type u_1} [inst : ] :
(fun x => x * 0) =

To match mul_one_eq_id.

theorem eq_zero_of_mul_self_eq_zero {M₀ : Type u_1} [inst : Mul M₀] [inst : Zero M₀] [inst : ] {a : M₀} (h : a * a = 0) :
a = 0
theorem mul_ne_zero {M₀ : Type u_1} [inst : Mul M₀] [inst : Zero M₀] [inst : ] {a : M₀} {b : M₀} (ha : a 0) (hb : b 0) :
a * b 0
instance NeZero.mul {M₀ : Type u_1} [inst : Zero M₀] [inst : Mul M₀] [inst : ] {x : M₀} {y : M₀} [inst : ] [inst : ] :
NeZero (x * y)
Equations
theorem eq_zero_of_zero_eq_one {M₀ : Type u_1} [inst : ] (h : 0 = 1) (a : M₀) :
a = 0

In a monoid with zero, if zero equals one, then zero is the only element.

def uniqueOfZeroEqOne {M₀ : Type u_1} [inst : ] (h : 0 = 1) :
Unique M₀

In a monoid with zero, if zero equals one, then zero is the unique element.

Somewhat arbitrarily, we define the default element to be 0. All other elements will be provably equal to it, but not necessarily definitionally equal.

Equations
• = { toInhabited := { default := 0 }, uniq := (_ : ∀ (a : M₀), a = 0) }
theorem subsingleton_iff_zero_eq_one {M₀ : Type u_1} [inst : ] :
0 = 1

In a monoid with zero, zero equals one if and only if all elements of that semiring are equal.

theorem subsingleton_of_zero_eq_one {M₀ : Type u_1} [inst : ] :
0 = 1

Alias of the forward direction of subsingleton_iff_zero_eq_one.

theorem eq_of_zero_eq_one {M₀ : Type u_1} [inst : ] (h : 0 = 1) (a : M₀) (b : M₀) :
a = b
theorem zero_ne_one_or_forall_eq_0 {M₀ : Type u_1} [inst : ] :
0 1 ∀ (a : M₀), a = 0

In a monoid with zero, either zero and one are nonequal, or zero is the only element.

theorem left_ne_zero_of_mul_eq_one {M₀ : Type u_1} [inst : ] [inst : ] {a : M₀} {b : M₀} (h : a * b = 1) :
a 0
theorem right_ne_zero_of_mul_eq_one {M₀ : Type u_1} [inst : ] [inst : ] {a : M₀} {b : M₀} (h : a * b = 1) :
b 0
instance CancelMonoidWithZero.to_noZeroDivisors {M₀ : Type u_1} [inst : ] :
Equations
theorem mul_left_inj' {M₀ : Type u_1} [inst : ] {a : M₀} {b : M₀} {c : M₀} (hc : c 0) :
a * c = b * c a = b
theorem mul_right_inj' {M₀ : Type u_1} [inst : ] {a : M₀} {b : M₀} {c : M₀} (ha : a 0) :
a * b = a * c b = c
@[simp]
theorem mul_eq_mul_right_iff {M₀ : Type u_1} [inst : ] {a : M₀} {b : M₀} {c : M₀} :
a * c = b * c a = b c = 0
@[simp]
theorem mul_eq_mul_left_iff {M₀ : Type u_1} [inst : ] {a : M₀} {b : M₀} {c : M₀} :
a * b = a * c b = c a = 0
theorem mul_right_eq_self₀ {M₀ : Type u_1} [inst : ] {a : M₀} {b : M₀} :
a * b = a b = 1 a = 0
theorem mul_left_eq_self₀ {M₀ : Type u_1} [inst : ] {a : M₀} {b : M₀} :
a * b = b a = 1 b = 0
theorem eq_zero_of_mul_eq_self_right {M₀ : Type u_1} [inst : ] {a : M₀} {b : M₀} (h₁ : b 1) (h₂ : a * b = a) :
a = 0

An element of a CancelMonoidWithZero fixed by right multiplication by an element other than one must be zero.

theorem eq_zero_of_mul_eq_self_left {M₀ : Type u_1} [inst : ] {a : M₀} {b : M₀} (h₁ : b 1) (h₂ : b * a = a) :
a = 0

An element of a CancelMonoidWithZero fixed by left multiplication by an element other than one must be zero.

@[simp]
theorem mul_inv_cancel_right₀ {G₀ : Type u_1} [inst : ] {b : G₀} (h : b 0) (a : G₀) :
a * b * b⁻¹ = a
@[simp]
theorem mul_inv_cancel_left₀ {G₀ : Type u_1} [inst : ] {a : G₀} (h : a 0) (b : G₀) :
a * (a⁻¹ * b) = b
theorem inv_ne_zero {G₀ : Type u_1} [inst : ] {a : G₀} (h : a 0) :
@[simp]
theorem inv_mul_cancel {G₀ : Type u_1} [inst : ] {a : G₀} (h : a 0) :
a⁻¹ * a = 1
theorem GroupWithZero.mul_left_injective {G₀ : Type u_1} [inst : ] {x : G₀} (h : x 0) :
Function.Injective fun y => x * y
theorem GroupWithZero.mul_right_injective {G₀ : Type u_1} [inst : ] {x : G₀} (h : x 0) :
Function.Injective fun y => y * x
@[simp]
theorem inv_mul_cancel_right₀ {G₀ : Type u_1} [inst : ] {b : G₀} (h : b 0) (a : G₀) :
a * b⁻¹ * b = a
@[simp]
theorem inv_mul_cancel_left₀ {G₀ : Type u_1} [inst : ] {a : G₀} (h : a 0) (b : G₀) :
a⁻¹ * (a * b) = b
instance GroupWithZero.toDivisionMonoid {G₀ : Type u_1} [inst : ] :
Equations
@[simp]
theorem zero_div {G₀ : Type u_1} [inst : ] (a : G₀) :
0 / a = 0
@[simp]
theorem div_zero {G₀ : Type u_1} [inst : ] (a : G₀) :
a / 0 = 0
@[simp]
theorem mul_self_mul_inv {G₀ : Type u_1} [inst : ] (a : G₀) :
a * a * a⁻¹ = a

Multiplying a by itself and then by its inverse results in a (whether or not a is zero).

@[simp]
theorem mul_inv_mul_self {G₀ : Type u_1} [inst : ] (a : G₀) :
a * a⁻¹ * a = a

Multiplying a by its inverse and then by itself results in a (whether or not a is zero).

@[simp]
theorem inv_mul_mul_self {G₀ : Type u_1} [inst : ] (a : G₀) :
a⁻¹ * a * a = a

Multiplying a⁻¹ by a twice results in a (whether or not a is zero).

@[simp]
theorem mul_self_div_self {G₀ : Type u_1} [inst : ] (a : G₀) :
a * a / a = a

Multiplying a by itself and then dividing by itself results in a, whether or not a is zero.

@[simp]
theorem div_self_mul_self {G₀ : Type u_1} [inst : ] (a : G₀) :
a / a * a = a

Dividing a by itself and then multiplying by itself results in a, whether or not a is zero.

@[simp]
theorem div_self_mul_self' {G₀ : Type u_1} [inst : ] (a : G₀) :
a / (a * a) = a⁻¹
theorem one_div_ne_zero {G₀ : Type u_1} [inst : ] {a : G₀} (h : a 0) :
1 / a 0
@[simp]
theorem inv_eq_zero {G₀ : Type u_1} [inst : ] {a : G₀} :
a⁻¹ = 0 a = 0
@[simp]
theorem zero_eq_inv {G₀ : Type u_1} [inst : ] {a : G₀} :
0 = a⁻¹ 0 = a
@[simp]
theorem div_div_self {G₀ : Type u_1} [inst : ] (a : G₀) :
a / (a / a) = a

Dividing a by the result of dividing a by itself results in a (whether or not a is zero).

theorem ne_zero_of_one_div_ne_zero {G₀ : Type u_1} [inst : ] {a : G₀} (h : 1 / a 0) :
a 0
theorem eq_zero_of_one_div_eq_zero {G₀ : Type u_1} [inst : ] {a : G₀} (h : 1 / a = 0) :
a = 0
theorem mul_left_surjective₀ {G₀ : Type u_1} [inst : ] {a : G₀} (h : a 0) :
Function.Surjective fun g => a * g
theorem mul_right_surjective₀ {G₀ : Type u_1} [inst : ] {a : G₀} (h : a 0) :
Function.Surjective fun g => g * a
theorem div_mul_eq_mul_div₀ {G₀ : Type u_1} [inst : ] (a : G₀) (b : G₀) (c : G₀) :
a / c * b = a * b / c

### Order dual #

instance instMulZeroClassOrderDual {α : Type u_1} [h : ] :
Equations
• instMulZeroClassOrderDual = h
instance instMulZeroOneClassOrderDual {α : Type u_1} [h : ] :
Equations
• instMulZeroOneClassOrderDual = h
instance instNoZeroDivisorsOrderDualInstMulOrderDualInstZeroOrderDual {α : Type u_1} [inst : Mul α] [inst : Zero α] [h : ] :
Equations
instance instSemigroupWithZeroOrderDual {α : Type u_1} [h : ] :
Equations
• instSemigroupWithZeroOrderDual = h
instance instMonoidWithZeroOrderDual {α : Type u_1} [h : ] :
Equations
• instMonoidWithZeroOrderDual = h
instance instCancelMonoidWithZeroOrderDual {α : Type u_1} [h : ] :
Equations
• instCancelMonoidWithZeroOrderDual = h
instance instCommMonoidWithZeroOrderDual {α : Type u_1} [h : ] :
Equations
• instCommMonoidWithZeroOrderDual = h
instance instCancelCommMonoidWithZeroOrderDual {α : Type u_1} [h : ] :
Equations
• instCancelCommMonoidWithZeroOrderDual = h
instance instGroupWithZeroOrderDual {α : Type u_1} [h : ] :
Equations
• instGroupWithZeroOrderDual = h
instance instCommGroupWithZeroOrderDual {α : Type u_1} [h : ] :
Equations
• instCommGroupWithZeroOrderDual = h

### Lexicographic order #

instance instMulZeroClassLex {α : Type u_1} [h : ] :
Equations
• instMulZeroClassLex = h
instance instMulZeroOneClassLex {α : Type u_1} [h : ] :
Equations
• instMulZeroOneClassLex = h
instance instNoZeroDivisorsLexInstMulLexInstZeroLex {α : Type u_1} [inst : Mul α] [inst : Zero α] [h : ] :
Equations
instance instSemigroupWithZeroLex {α : Type u_1} [h : ] :
Equations
• instSemigroupWithZeroLex = h
instance instMonoidWithZeroLex {α : Type u_1} [h : ] :
Equations
• instMonoidWithZeroLex = h
instance instCancelMonoidWithZeroLex {α : Type u_1} [h : ] :
Equations
• instCancelMonoidWithZeroLex = h
instance instCommMonoidWithZeroLex {α : Type u_1} [h : ] :
Equations
• instCommMonoidWithZeroLex = h
instance instCancelCommMonoidWithZeroLex {α : Type u_1} [h : ] :
Equations
• instCancelCommMonoidWithZeroLex = h
instance instGroupWithZeroLex {α : Type u_1} [h : ] :
Equations
• instGroupWithZeroLex = h
instance instCommGroupWithZeroLex {α : Type u_1} [h : ] :
Equations
• instCommGroupWithZeroLex = h