mathlib documentation

algebra.group_with_zero

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:

Main definitions

Implementation details

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

@[instance]
def mul_zero_class.to_has_mul (M₀ : Type u_5) [s : mul_zero_class M₀] :
has_mul M₀

@[class]
structure mul_zero_class  :
Type u_5Type u_5
  • mul : M₀ → M₀ → M₀
  • zero : M₀
  • zero_mul : ∀ (a : M₀), 0 * a = 0
  • 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₀.

Instances
@[instance]
def mul_zero_class.to_has_zero (M₀ : Type u_5) [s : mul_zero_class M₀] :

@[simp]
theorem zero_mul {M₀ : Type u_1} [mul_zero_class M₀] (a : M₀) :
0 * a = 0

@[simp]
theorem mul_zero {M₀ : Type u_1} [mul_zero_class M₀] (a : M₀) :
a * 0 = 0

def function.injective.mul_zero_class {M₀ : Type u_1} {M₀' : Type u_3} [mul_zero_class M₀] [has_mul M₀'] [has_zero M₀'] (f : M₀' → M₀) :
function.injective ff 0 = 0(∀ (a b : M₀'), f (a * b) = (f a) * f b)mul_zero_class M₀'

Pullback a mul_zero_class instance along an injective function.

Equations
def function.surjective.mul_zero_class {M₀ : Type u_1} {M₀' : Type u_3} [mul_zero_class M₀] [has_mul M₀'] [has_zero M₀'] (f : M₀ → M₀') :
function.surjective ff 0 = 0(∀ (a b : M₀), f (a * b) = (f a) * f b)mul_zero_class M₀'

Pushforward a mul_zero_class instance along an surjective function.

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

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

theorem left_ne_zero_of_mul {M₀ : Type u_1} [mul_zero_class M₀] {a b : M₀} :
a * b 0a 0

theorem right_ne_zero_of_mul {M₀ : Type u_1} [mul_zero_class M₀] {a b : M₀} :
a * b 0b 0

theorem ne_zero_and_ne_zero_of_mul {M₀ : Type u_1} [mul_zero_class M₀] {a b : M₀} :
a * b 0a 0 b 0

theorem mul_eq_zero_of_ne_zero_imp_eq_zero {M₀ : Type u_1} [mul_zero_class M₀] {a b : M₀} :
(a 0b = 0)a * b = 0

@[class]
structure no_zero_divisors (M₀ : Type u_5) [has_mul M₀] [has_zero M₀] :
Prop
  • eq_zero_or_eq_zero_of_mul_eq_zero : ∀ {a b : M₀}, a * b = 0a = 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₀.

Instances
theorem function.injective.no_zero_divisors {M₀ : Type u_1} {M₀' : Type u_3} [has_mul M₀] [has_zero M₀] [has_mul M₀'] [has_zero M₀'] [no_zero_divisors M₀'] (f : M₀ → M₀') :
function.injective ff 0 = 0(∀ (x y : M₀), f (x * y) = (f x) * f y)no_zero_divisors M₀

Pushforward a no_zero_divisors instance along an injective function.

theorem eq_zero_of_mul_self_eq_zero {M₀ : Type u_1} [has_mul M₀] [has_zero M₀] [no_zero_divisors M₀] {a : M₀} :
a * a = 0a = 0

@[simp]
theorem mul_eq_zero {M₀ : Type u_1} [mul_zero_class M₀] [no_zero_divisors 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} [mul_zero_class M₀] [no_zero_divisors 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} [mul_zero_class M₀] [no_zero_divisors 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_ne_zero {M₀ : Type u_1} [mul_zero_class M₀] [no_zero_divisors M₀] {a b : M₀} :
a 0b 0a * b 0

theorem mul_eq_zero_comm {M₀ : Type u_1} [mul_zero_class M₀] [no_zero_divisors 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} [mul_zero_class M₀] [no_zero_divisors 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} [mul_zero_class M₀] [no_zero_divisors M₀] {a : M₀} :
a * a = 0 a = 0

theorem zero_eq_mul_self {M₀ : Type u_1} [mul_zero_class M₀] [no_zero_divisors M₀] {a : M₀} :
0 = a * a a = 0

@[instance]
def monoid_with_zero.to_mul_zero_class (M₀ : Type u_5) [s : monoid_with_zero M₀] :

@[instance]
def monoid_with_zero.to_monoid (M₀ : Type u_5) [s : monoid_with_zero M₀] :
monoid M₀

@[class]
structure monoid_with_zero  :
Type u_5Type u_5
  • mul : M₀ → M₀ → M₀
  • mul_assoc : ∀ (a b c_1 : M₀), (a * b) * c_1 = a * b * c_1
  • one : 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

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

Instances
@[class]
structure cancel_monoid_with_zero  :
Type u_5Type u_5
  • mul : M₀ → M₀ → M₀
  • mul_assoc : ∀ (a b c_1 : M₀), (a * b) * c_1 = a * b * c_1
  • one : 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
  • mul_left_cancel_of_ne_zero : ∀ {a b c_1 : M₀}, a 0a * b = a * c_1b = c_1
  • mul_right_cancel_of_ne_zero : ∀ {a b c_1 : M₀}, b 0a * b = c_1 * ba = c_1

A type M is a cancel_monoid_with_zero 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
@[simp]
theorem zero_ne_one {M₀ : Type u_1} [monoid_with_zero M₀] [nontrivial M₀] :
0 1

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

@[simp]
theorem one_ne_zero {M₀ : Type u_1} [monoid_with_zero M₀] [nontrivial M₀] :
1 0

theorem ne_zero_of_eq_one {M₀ : Type u_1} [monoid_with_zero M₀] [nontrivial M₀] {a : M₀} :
a = 1a 0

theorem left_ne_zero_of_mul_eq_one {M₀ : Type u_1} [monoid_with_zero M₀] [nontrivial M₀] {a b : M₀} :
a * b = 1a 0

theorem right_ne_zero_of_mul_eq_one {M₀ : Type u_1} [monoid_with_zero M₀] [nontrivial M₀] {a b : M₀} :
a * b = 1b 0

theorem pullback_nonzero {M₀ : Type u_1} {M₀' : Type u_3} [monoid_with_zero M₀] [nontrivial M₀] [has_zero M₀'] [has_one M₀'] (f : M₀' → M₀) :
f 0 = 0f 1 = 1nontrivial M₀'

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

@[instance]

@[instance]

@[class]
structure comm_monoid_with_zero  :
Type u_5Type u_5
  • mul : M₀ → M₀ → M₀
  • mul_assoc : ∀ (a b c_1 : M₀), (a * b) * c_1 = a * b * c_1
  • one : M₀
  • one_mul : ∀ (a : M₀), 1 * a = a
  • mul_one : ∀ (a : M₀), a * 1 = a
  • 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

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.

Instances
@[class]
structure comm_cancel_monoid_with_zero  :
Type u_5Type u_5
  • mul : M₀ → M₀ → M₀
  • mul_assoc : ∀ (a b c_1 : M₀), (a * b) * c_1 = a * b * c_1
  • one : M₀
  • one_mul : ∀ (a : M₀), 1 * a = a
  • mul_one : ∀ (a : M₀), a * 1 = a
  • 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 b c_1 : M₀}, a 0a * b = a * c_1b = c_1
  • mul_right_cancel_of_ne_zero : ∀ {a b c_1 : M₀}, b 0a * b = c_1 * ba = c_1

A type M is a comm_cancel_monoid_with_zero 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]
def group_with_zero.to_nontrivial (G₀ : Type u_5) [s : group_with_zero G₀] :

@[instance]
def group_with_zero.to_monoid_with_zero (G₀ : Type u_5) [s : group_with_zero G₀] :

@[instance]
def group_with_zero.to_has_inv (G₀ : Type u_5) [s : group_with_zero G₀] :
has_inv G₀

@[class]
structure group_with_zero  :
Type u_5Type u_5
  • mul : G₀ → G₀ → G₀
  • mul_assoc : ∀ (a b c_1 : G₀), (a * b) * c_1 = a * b * c_1
  • one : G₀
  • one_mul : ∀ (a : G₀), 1 * a = a
  • mul_one : ∀ (a : G₀), a * 1 = a
  • zero : G₀
  • zero_mul : ∀ (a : G₀), 0 * a = 0
  • mul_zero : ∀ (a : G₀), a * 0 = 0
  • inv : G₀ → G₀
  • exists_pair_ne : ∃ (x y : G₀), x y
  • inv_zero : 0⁻¹ = 0
  • mul_inv_cancel : ∀ (a : G₀), a 0a * 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.

Instances
@[class]
structure comm_group_with_zero  :
Type u_5Type u_5
  • mul : G₀ → G₀ → G₀
  • mul_assoc : ∀ (a b c_1 : G₀), (a * b) * c_1 = a * b * c_1
  • one : G₀
  • one_mul : ∀ (a : G₀), 1 * a = a
  • mul_one : ∀ (a : G₀), a * 1 = a
  • 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₀
  • exists_pair_ne : ∃ (x y : G₀), x y
  • inv_zero : 0⁻¹ = 0
  • mul_inv_cancel : ∀ (a : G₀), a 0a * 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.

Instances
@[instance]

@[instance]
def group_with_zero.has_div {G₀ : Type u_1} [group_with_zero G₀] :
has_div G₀

The division operation on a group with zero element.

Equations
def function.injective.monoid_with_zero {M₀ : Type u_1} {M₀' : Type u_3} [has_zero M₀'] [has_mul M₀'] [has_one M₀'] [monoid_with_zero M₀] (f : M₀' → M₀) :
function.injective ff 0 = 0f 1 = 1(∀ (x y : M₀'), f (x * y) = (f x) * f y)monoid_with_zero M₀'

Pullback a monoid_with_zero class along an injective function.

Equations
def function.surjective.monoid_with_zero {M₀ : Type u_1} {M₀' : Type u_3} [has_zero M₀'] [has_mul M₀'] [has_one M₀'] [monoid_with_zero M₀] (f : M₀ → M₀') :
function.surjective ff 0 = 0f 1 = 1(∀ (x y : M₀), f (x * y) = (f x) * f y)monoid_with_zero M₀'

Pushforward a monoid_with_zero class along a surjective function.

Equations
def function.injective.comm_monoid_with_zero {M₀ : Type u_1} {M₀' : Type u_3} [has_zero M₀'] [has_mul M₀'] [has_one M₀'] [comm_monoid_with_zero M₀] (f : M₀' → M₀) :
function.injective ff 0 = 0f 1 = 1(∀ (x y : M₀'), f (x * y) = (f x) * f y)comm_monoid_with_zero M₀'

Pullback a monoid_with_zero class along an injective function.

Equations
def function.surjective.comm_monoid_with_zero {M₀ : Type u_1} {M₀' : Type u_3} [has_zero M₀'] [has_mul M₀'] [has_one M₀'] [comm_monoid_with_zero M₀] (f : M₀ → M₀') :
function.surjective ff 0 = 0f 1 = 1(∀ (x y : M₀), f (x * y) = (f x) * f y)comm_monoid_with_zero M₀'

Pushforward a monoid_with_zero class along a surjective function.

Equations
@[simp]
theorem units.ne_zero {M₀ : Type u_1} [monoid_with_zero M₀] [nontrivial M₀] (u : units M₀) :
u 0

An element of the unit group of a nonzero monoid with zero represented as an element of the monoid is nonzero.

@[simp]
theorem units.mul_left_eq_zero {M₀ : Type u_1} [monoid_with_zero M₀] (u : units M₀) {a : M₀} :
a * u = 0 a = 0

@[simp]
theorem units.mul_right_eq_zero {M₀ : Type u_1} [monoid_with_zero M₀] (u : units M₀) {a : M₀} :
(u) * a = 0 a = 0

theorem is_unit.ne_zero {M₀ : Type u_1} [monoid_with_zero M₀] [nontrivial M₀] {a : M₀} :
is_unit aa 0

theorem is_unit.mul_right_eq_zero {M₀ : Type u_1} [monoid_with_zero M₀] {a b : M₀} :
is_unit a(a * b = 0 b = 0)

theorem is_unit.mul_left_eq_zero {M₀ : Type u_1} [monoid_with_zero M₀] {a b : M₀} :
is_unit b(a * b = 0 a = 0)

theorem eq_zero_of_zero_eq_one {M₀ : Type u_1} [monoid_with_zero M₀] (h : 0 = 1) (a : M₀) :
a = 0

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

def unique_of_zero_eq_one {M₀ : Type u_1} [monoid_with_zero M₀] :
0 = 1unique 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
theorem subsingleton_iff_zero_eq_one {M₀ : Type u_1} [monoid_with_zero M₀] :
0 = 1 subsingleton M₀

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

theorem eq_of_zero_eq_one {M₀ : Type u_1} [monoid_with_zero M₀] (h : 0 = 1) (a b : M₀) :
a = b

@[simp]
theorem is_unit_zero_iff {M₀ : Type u_1} [monoid_with_zero M₀] :
is_unit 0 0 = 1

@[simp]
theorem not_is_unit_zero {M₀ : Type u_1} [monoid_with_zero M₀] [nontrivial M₀] :

theorem zero_ne_one_or_forall_eq_0 (M₀ : Type u_1) [monoid_with_zero M₀] :
0 1 ∀ (a : M₀), a = 0

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

theorem mul_left_cancel' {M₀ : Type u_1} [cancel_monoid_with_zero M₀] {a b c : M₀} :
a 0a * b = a * cb = c

theorem mul_right_cancel' {M₀ : Type u_1} [cancel_monoid_with_zero M₀] {a b c : M₀} :
b 0a * b = c * ba = c

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

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

@[simp]
theorem mul_eq_mul_right_iff {M₀ : Type u_1} [cancel_monoid_with_zero M₀] {a b c : M₀} :
a * c = b * c a = b c = 0

@[simp]
theorem mul_eq_mul_left_iff {M₀ : Type u_1} [cancel_monoid_with_zero M₀] {a b c : M₀} :
a * b = a * c b = c a = 0

def function.injective.cancel_monoid_with_zero {M₀ : Type u_1} {M₀' : Type u_3} [cancel_monoid_with_zero M₀] [has_zero M₀'] [has_mul M₀'] [has_one M₀'] (f : M₀' → M₀) :
function.injective ff 0 = 0f 1 = 1(∀ (x y : M₀'), f (x * y) = (f x) * f y)cancel_monoid_with_zero M₀'

Pullback a monoid_with_zero class along an injective function.

Equations
theorem eq_zero_of_mul_eq_self_right {M₀ : Type u_1} [cancel_monoid_with_zero M₀] {a b : M₀} :
b 1a * b = aa = 0

An element of a cancel_monoid_with_zero 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} [cancel_monoid_with_zero M₀] {a b : M₀} :
b 1b * a = aa = 0

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

theorem div_eq_mul_inv {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :
a / b = a * b⁻¹

@[simp]
theorem inv_zero {G₀ : Type u_2} [group_with_zero G₀] :
0⁻¹ = 0

@[simp]
theorem mul_inv_cancel {G₀ : Type u_2} [group_with_zero G₀] {a : G₀} :
a 0a * a⁻¹ = 1

def function.injective.group_with_zero {G₀ : Type u_2} {G₀' : Type u_4} [group_with_zero G₀] [has_zero G₀'] [has_mul G₀'] [has_one G₀'] [has_inv G₀'] (f : G₀' → G₀) :
function.injective ff 0 = 0f 1 = 1(∀ (x y : G₀'), f (x * y) = (f x) * f y)(∀ (x : G₀'), f x⁻¹ = (f x)⁻¹)group_with_zero G₀'

Pullback a group_with_zero class along an injective function.

Equations
def function.surjective.group_with_zero {G₀ : Type u_2} {G₀' : Type u_4} [group_with_zero G₀] [has_zero G₀'] [has_mul G₀'] [has_one G₀'] [has_inv G₀'] (h01 : 0 1) (f : G₀ → G₀') :
function.surjective ff 0 = 0f 1 = 1(∀ (x y : G₀), f (x * y) = (f x) * f y)(∀ (x : G₀), f x⁻¹ = (f x)⁻¹)group_with_zero G₀'

Pushforward a group_with_zero class along an surjective function.

Equations
@[simp]
theorem mul_inv_cancel_right' {G₀ : Type u_2} [group_with_zero G₀] {b : G₀} (h : b 0) (a : G₀) :
(a * b) * b⁻¹ = a

@[simp]
theorem mul_inv_cancel_left' {G₀ : Type u_2} [group_with_zero G₀] {a : G₀} (h : a 0) (b : G₀) :
a * a⁻¹ * b = b

theorem inv_ne_zero {G₀ : Type u_2} [group_with_zero G₀] {a : G₀} :
a 0a⁻¹ 0

@[simp]
theorem inv_mul_cancel {G₀ : Type u_2} [group_with_zero G₀] {a : G₀} :
a 0a⁻¹ * a = 1

@[simp]
theorem inv_mul_cancel_right' {G₀ : Type u_2} [group_with_zero G₀] {b : G₀} (h : b 0) (a : G₀) :
(a * b⁻¹) * b = a

@[simp]
theorem inv_mul_cancel_left' {G₀ : Type u_2} [group_with_zero G₀] {a : G₀} (h : a 0) (b : G₀) :
a⁻¹ * a * b = b

@[simp]
theorem inv_one {G₀ : Type u_2} [group_with_zero G₀] :
1⁻¹ = 1

@[simp]
theorem inv_inv' {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) :

@[simp]
theorem mul_self_mul_inv {G₀ : Type u_2} [group_with_zero G₀] (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_2} [group_with_zero G₀] (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_2} [group_with_zero G₀] (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_2} [group_with_zero G₀] (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_2} [group_with_zero G₀] (a : G₀) :
(a / a) * a = a

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

theorem eq_inv_of_mul_right_eq_one {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :
a * b = 1b = a⁻¹

theorem eq_inv_of_mul_left_eq_one {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :
a * b = 1a = b⁻¹

@[simp]
theorem inv_inj' {G₀ : Type u_2} [group_with_zero G₀] {g h : G₀} :
g⁻¹ = h⁻¹ g = h

theorem inv_eq_iff {G₀ : Type u_2} [group_with_zero G₀] {g h : G₀} :
g⁻¹ = h h⁻¹ = g

@[simp]
theorem inv_eq_one' {G₀ : Type u_2} [group_with_zero G₀] {g : G₀} :
g⁻¹ = 1 g = 1

def units.mk0 {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) :
a 0units G₀

Embed a non-zero element of a group_with_zero into the unit group. By combining this function with the operations on units, or the /ₚ operation, it is possible to write a division as a partial function with three arguments.

Equations
@[simp]
theorem units.coe_mk0 {G₀ : Type u_2} [group_with_zero G₀] {a : G₀} (h : a 0) :
(units.mk0 a h) = a

@[simp]
theorem units.mk0_coe {G₀ : Type u_2} [group_with_zero G₀] (u : units G₀) (h : u 0) :

@[simp]
theorem units.coe_inv' {G₀ : Type u_2} [group_with_zero G₀] (u : units G₀) :

@[simp]
theorem units.mul_inv' {G₀ : Type u_2} [group_with_zero G₀] (u : units G₀) :
(u) * (u)⁻¹ = 1

@[simp]
theorem units.inv_mul' {G₀ : Type u_2} [group_with_zero G₀] (u : units G₀) :
(u)⁻¹ * u = 1

@[simp]
theorem units.mk0_inj {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} (ha : a 0) (hb : b 0) :
units.mk0 a ha = units.mk0 b hb a = b

@[simp]
theorem units.exists_iff_ne_zero {G₀ : Type u_2} [group_with_zero G₀] {x : G₀} :
(∃ (u : units G₀), u = x) x 0

theorem is_unit.mk0 {G₀ : Type u_2} [group_with_zero G₀] (x : G₀) :
x 0is_unit x

theorem is_unit_iff_ne_zero {G₀ : Type u_2} [group_with_zero G₀] {x : G₀} :

@[instance]

theorem mul_inv_rev' {G₀ : Type u_2} [group_with_zero G₀] (x y : G₀) :
(x * y)⁻¹ = y⁻¹ * x⁻¹

@[simp]
theorem div_self {G₀ : Type u_2} [group_with_zero G₀] {a : G₀} :
a 0a / a = 1

@[simp]
theorem div_one {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) :
a / 1 = a

@[simp]
theorem one_div {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) :
1 / a = a⁻¹

@[simp]
theorem zero_div {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) :
0 / a = 0

@[simp]
theorem div_zero {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) :
a / 0 = 0

@[simp]
theorem div_mul_cancel {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) {b : G₀} :
b 0(a / b) * b = a

theorem div_mul_cancel_of_imp {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :
(b = 0a = 0)(a / b) * b = a

@[simp]
theorem mul_div_cancel {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) {b : G₀} :
b 0a * b / b = a

theorem mul_div_cancel_of_imp {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :
(b = 0a = 0)a * b / b = a

theorem mul_div_assoc {G₀ : Type u_2} [group_with_zero G₀] {a b c : G₀} :
a * b / c = a * (b / c)

theorem div_eq_mul_one_div {G₀ : Type u_2} [group_with_zero G₀] (a b : G₀) :
a / b = a * (1 / b)

theorem mul_one_div_cancel {G₀ : Type u_2} [group_with_zero G₀] {a : G₀} :
a 0a * (1 / a) = 1

theorem one_div_mul_cancel {G₀ : Type u_2} [group_with_zero G₀] {a : G₀} :
a 0(1 / a) * a = 1

theorem one_div_one {G₀ : Type u_2} [group_with_zero G₀] :
1 / 1 = 1

theorem one_div_ne_zero {G₀ : Type u_2} [group_with_zero G₀] {a : G₀} :
a 01 / a 0

theorem eq_one_div_of_mul_eq_one {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :
a * b = 1b = 1 / a

theorem eq_one_div_of_mul_eq_one_left {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :
b * a = 1b = 1 / a

@[simp]
theorem one_div_div {G₀ : Type u_2} [group_with_zero G₀] (a b : G₀) :
1 / (a / b) = b / a

theorem one_div_one_div {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) :
1 / (1 / a) = a

theorem eq_of_one_div_eq_one_div {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :
1 / a = 1 / ba = b

@[simp]
theorem inv_eq_zero {G₀ : Type u_2} [group_with_zero G₀] {a : G₀} :
a⁻¹ = 0 a = 0

@[simp]
theorem zero_eq_inv {G₀ : Type u_2} [group_with_zero G₀] {a : G₀} :
0 = a⁻¹ 0 = a

theorem one_div_mul_one_div_rev {G₀ : Type u_2} [group_with_zero G₀] (a b : G₀) :
(1 / a) * (1 / b) = 1 / b * a

theorem divp_eq_div {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) (u : units G₀) :
a /ₚ u = a / u

@[simp]
theorem divp_mk0 {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) {b : G₀} (hb : b 0) :
a /ₚ units.mk0 b hb = a / b

theorem inv_div {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :
(a / b)⁻¹ = b / a

theorem inv_div_left {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :
a⁻¹ / b = (b * a)⁻¹

theorem div_ne_zero {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :
a 0b 0a / b 0

@[simp]
theorem div_eq_zero_iff {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :
a / b = 0 a = 0 b = 0

theorem div_ne_zero_iff {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :
a / b 0 a 0 b 0

theorem div_left_inj' {G₀ : Type u_2} [group_with_zero G₀] {a b c : G₀} :
c 0(a / c = b / c a = b)

theorem div_eq_iff_mul_eq {G₀ : Type u_2} [group_with_zero G₀] {a b c : G₀} :
b 0(a / b = c c * b = a)

theorem eq_div_iff_mul_eq {G₀ : Type u_2} [group_with_zero G₀] {a b c : G₀} :
c 0(a = b / c a * c = b)

theorem div_eq_of_eq_mul {G₀ : Type u_2} [group_with_zero G₀] {x : G₀} (hx : x 0) {y z : G₀} :
y = z * xy / x = z

theorem eq_div_of_mul_eq {G₀ : Type u_2} [group_with_zero G₀] {x : G₀} (hx : x 0) {y z : G₀} :
z * x = yz = y / x

theorem eq_of_div_eq_one {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :
a / b = 1a = b

theorem div_eq_one_iff_eq {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :
b 0(a / b = 1 a = b)

theorem div_mul_left {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :
b 0b / a * b = 1 / a

theorem mul_div_mul_right {G₀ : Type u_2} [group_with_zero G₀] (a b : G₀) {c : G₀} :
c 0a * c / b * c = a / b

theorem mul_mul_div {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) {b : G₀} :
b 0a = (a * b) * (1 / b)

def function.injective.comm_group_with_zero {G₀ : Type u_2} {G₀' : Type u_4} [comm_group_with_zero G₀] [has_zero G₀'] [has_mul G₀'] [has_one G₀'] [has_inv G₀'] (f : G₀' → G₀) :
function.injective ff 0 = 0f 1 = 1(∀ (x y : G₀'), f (x * y) = (f x) * f y)(∀ (x : G₀'), f x⁻¹ = (f x)⁻¹)comm_group_with_zero G₀'

Pullback a comm_group_with_zero class along an injective function.

Equations
def function.surjective.comm_group_with_zero {G₀ : Type u_2} {G₀' : Type u_4} [comm_group_with_zero G₀] [has_zero G₀'] [has_mul G₀'] [has_one G₀'] [has_inv G₀'] (h01 : 0 1) (f : G₀ → G₀') :
function.surjective ff 0 = 0f 1 = 1(∀ (x y : G₀), f (x * y) = (f x) * f y)(∀ (x : G₀), f x⁻¹ = (f x)⁻¹)comm_group_with_zero G₀'

Pushforward a comm_group_with_zero class along an surjective function.

Equations
theorem mul_inv' {G₀ : Type u_2} [comm_group_with_zero G₀] {a b : G₀} :
(a * b)⁻¹ = a⁻¹ * b⁻¹

theorem one_div_mul_one_div {G₀ : Type u_2} [comm_group_with_zero G₀] (a b : G₀) :
(1 / a) * (1 / b) = 1 / a * b

theorem div_mul_right {G₀ : Type u_2} [comm_group_with_zero G₀] {a : G₀} (b : G₀) :
a 0a / a * b = 1 / b

theorem mul_div_cancel_left_of_imp {G₀ : Type u_2} [comm_group_with_zero G₀] {a b : G₀} :
(a = 0b = 0)a * b / a = b

theorem mul_div_cancel_left {G₀ : Type u_2} [comm_group_with_zero G₀] {a : G₀} (b : G₀) :
a 0a * b / a = b

theorem mul_div_cancel_of_imp' {G₀ : Type u_2} [comm_group_with_zero G₀] {a b : G₀} :
(b = 0a = 0)b * (a / b) = a

theorem mul_div_cancel' {G₀ : Type u_2} [comm_group_with_zero G₀] (a : G₀) {b : G₀} :
b 0b * (a / b) = a

theorem div_mul_div {G₀ : Type u_2} [comm_group_with_zero G₀] (a b c d : G₀) :
(a / b) * (c / d) = a * c / b * d

theorem mul_div_mul_left {G₀ : Type u_2} [comm_group_with_zero G₀] (a b : G₀) {c : G₀} :
c 0c * a / c * b = a / b

theorem div_mul_eq_mul_div {G₀ : Type u_2} [comm_group_with_zero G₀] (a b c : G₀) :
(b / c) * a = b * a / c

theorem div_mul_eq_mul_div_comm {G₀ : Type u_2} [comm_group_with_zero G₀] (a b c : G₀) :
(b / c) * a = b * (a / c)

theorem mul_eq_mul_of_div_eq_div {G₀ : Type u_2} [comm_group_with_zero G₀] (a : G₀) {b : G₀} (c : G₀) {d : G₀} :
b 0d 0a / b = c / da * d = c * b

theorem div_div_eq_mul_div {G₀ : Type u_2} [comm_group_with_zero G₀] (a b c : G₀) :
a / (b / c) = a * c / b

theorem div_div_eq_div_mul {G₀ : Type u_2} [comm_group_with_zero G₀] (a b c : G₀) :
a / b / c = a / b * c

theorem div_div_div_div_eq {G₀ : Type u_2} [comm_group_with_zero G₀] (a : G₀) {b c d : G₀} :
a / b / (c / d) = a * d / b * c

theorem div_mul_eq_div_mul_one_div {G₀ : Type u_2} [comm_group_with_zero G₀] (a b c : G₀) :
a / b * c = (a / b) * (1 / c)

@[simp]
theorem div_div_self {G₀ : Type u_2} [comm_group_with_zero G₀] (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_2} [comm_group_with_zero G₀] {a : G₀} :
1 / a 0a 0

theorem eq_zero_of_one_div_eq_zero {G₀ : Type u_2} [comm_group_with_zero G₀] {a : G₀} :
1 / a = 0a = 0

theorem div_helper {G₀ : Type u_2} [comm_group_with_zero G₀] {a : G₀} (b : G₀) :
a 0(1 / a * b) * a = 1 / b

theorem div_eq_inv_mul {G₀ : Type u_2} [comm_group_with_zero G₀] {a b : G₀} :
a / b = b⁻¹ * a

theorem mul_div_right_comm {G₀ : Type u_2} [comm_group_with_zero G₀] (a b c : G₀) :
a * b / c = (a / c) * b

theorem mul_comm_div' {G₀ : Type u_2} [comm_group_with_zero G₀] (a b c : G₀) :
(a / b) * c = a * (c / b)

theorem div_mul_comm' {G₀ : Type u_2} [comm_group_with_zero G₀] (a b c : G₀) :
(a / b) * c = (c / b) * a

theorem mul_div_comm {G₀ : Type u_2} [comm_group_with_zero G₀] (a b c : G₀) :
a * (b / c) = b * (a / c)

theorem div_right_comm {G₀ : Type u_2} [comm_group_with_zero G₀] {b c : G₀} (a : G₀) :
a / b / c = a / c / b

theorem div_div_div_cancel_right {G₀ : Type u_2} [comm_group_with_zero G₀] {b c : G₀} (a : G₀) :
c 0a / c / (b / c) = a / b

theorem div_mul_div_cancel {G₀ : Type u_2} [comm_group_with_zero G₀] {b c : G₀} (a : G₀) :
c 0(a / c) * (c / b) = a / b

theorem div_eq_div_iff {G₀ : Type u_2} [comm_group_with_zero G₀] {a b c d : G₀} :
b 0d 0(a / b = c / d a * d = c * b)

theorem div_eq_iff {G₀ : Type u_2} [comm_group_with_zero G₀] {a b c : G₀} :
b 0(a / b = c a = c * b)

theorem eq_div_iff {G₀ : Type u_2} [comm_group_with_zero G₀] {a b c : G₀} :
b 0(c = a / b c * b = a)

theorem div_div_cancel' {G₀ : Type u_2} [comm_group_with_zero G₀] {a b : G₀} :
a 0a / (a / b) = b

@[simp]
theorem semiconj_by.zero_right {G₀ : Type u_2} [mul_zero_class G₀] (a : G₀) :

@[simp]
theorem semiconj_by.zero_left {G₀ : Type u_2} [mul_zero_class G₀] (x y : G₀) :

@[simp]
theorem semiconj_by.inv_symm_left_iff' {G₀ : Type u_2} [group_with_zero G₀] {a x y : G₀} :

theorem semiconj_by.inv_symm_left' {G₀ : Type u_2} [group_with_zero G₀] {a x y : G₀} :

theorem semiconj_by.inv_right' {G₀ : Type u_2} [group_with_zero G₀] {a x y : G₀} :

@[simp]
theorem semiconj_by.inv_right_iff' {G₀ : Type u_2} [group_with_zero G₀] {a x y : G₀} :

theorem semiconj_by.div_right {G₀ : Type u_2} [group_with_zero G₀] {a x y x' y' : G₀} :
semiconj_by a x ysemiconj_by a x' y'semiconj_by a (x / x') (y / y')

@[simp]
theorem commute.zero_right {G₀ : Type u_2} [mul_zero_class G₀] (a : G₀) :

@[simp]
theorem commute.zero_left {G₀ : Type u_2} [mul_zero_class G₀] (a : G₀) :

@[simp]
theorem commute.inv_left_iff' {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :

theorem commute.inv_left' {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :
commute a bcommute a⁻¹ b

@[simp]
theorem commute.inv_right_iff' {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :

theorem commute.inv_right' {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :
commute a bcommute a b⁻¹

theorem commute.inv_inv' {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} :

@[simp]
theorem commute.div_right {G₀ : Type u_2} [group_with_zero G₀] {a b c : G₀} :
commute a bcommute a ccommute a (b / c)

@[simp]
theorem commute.div_left {G₀ : Type u_2} [group_with_zero G₀] {a b c : G₀} :
commute a ccommute b ccommute (a / b) c

theorem monoid_hom.map_ne_zero {M₀ : Type u_1} {G₀ : Type u_2} [group_with_zero G₀] [monoid_with_zero M₀] [nontrivial M₀] (f : G₀ →* M₀) (h0 : f 0 = 0) {a : G₀} :
f a 0 a 0

theorem monoid_hom.map_eq_zero {M₀ : Type u_1} {G₀ : Type u_2} [group_with_zero G₀] [monoid_with_zero M₀] [nontrivial M₀] (f : G₀ →* M₀) (h0 : f 0 = 0) {a : G₀} :
f a = 0 a = 0

theorem monoid_hom.map_inv' {G₀ : Type u_2} {G₀' : Type u_4} [group_with_zero G₀] [group_with_zero G₀'] (f : G₀ →* G₀') (h0 : f 0 = 0) (a : G₀) :

A monoid homomorphism between groups with zeros sending 0 to 0 sends a⁻¹ to (f a)⁻¹.

theorem monoid_hom.map_div {G₀ : Type u_2} {G₀' : Type u_4} [group_with_zero G₀] [group_with_zero G₀'] (f : G₀ →* G₀') (h0 : f 0 = 0) (a b : G₀) :
f (a / b) = f a / f b

@[simp]
theorem monoid_hom.map_units_inv {M : Type u_1} {G₀ : Type u_2} [monoid M] [group_with_zero G₀] (f : M →* G₀) (u : units M) :