# mathlibdocumentation

algebra.group_with_zero.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 `group_with_zero` and `comm_group_with_zero`. To reduce import dependencies, the type-classes themselves are in `algebra.group_with_zero.defs`.

## Implementation details #

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

@[protected, reducible]
def function.injective.mul_zero_class {M₀ : Type u_2} {M₀' : Type u_4} [mul_zero_class M₀] [has_mul M₀'] [has_zero M₀'] (f : M₀' → M₀) (hf : function.injective f) (zero : f 0 = 0) (mul : ∀ (a b : M₀'), f (a * b) = f a * f b) :

Pullback a `mul_zero_class` instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.mul_zero_class {M₀ : Type u_2} {M₀' : Type u_4} [mul_zero_class M₀] [has_mul M₀'] [has_zero M₀'] (f : M₀ → M₀') (hf : function.surjective f) (zero : f 0 = 0) (mul : ∀ (a b : M₀), f (a * b) = f a * f b) :

Pushforward a `mul_zero_class` instance along an surjective function. See note [reducible non-instances].

Equations
theorem mul_eq_zero_of_left {M₀ : Type u_2} [mul_zero_class M₀] {a : M₀} (h : a = 0) (b : M₀) :
a * b = 0
theorem mul_eq_zero_of_right {M₀ : Type u_2} [mul_zero_class M₀] {b : M₀} (a : M₀) (h : b = 0) :
a * b = 0
theorem left_ne_zero_of_mul {M₀ : Type u_2} [mul_zero_class M₀] {a b : M₀} :
a * b 0a 0
theorem right_ne_zero_of_mul {M₀ : Type u_2} [mul_zero_class M₀] {a b : M₀} :
a * b 0b 0
theorem ne_zero_and_ne_zero_of_mul {M₀ : Type u_2} [mul_zero_class M₀] {a b : M₀} (h : a * b 0) :
a 0 b 0
theorem mul_eq_zero_of_ne_zero_imp_eq_zero {M₀ : Type u_2} [mul_zero_class M₀] {a b : M₀} (h : a 0b = 0) :
a * b = 0
theorem zero_mul_eq_const {M₀ : Type u_2} [mul_zero_class M₀] :
= 0

To match `one_mul_eq_id`.

theorem mul_zero_eq_const {M₀ : Type u_2} [mul_zero_class M₀] :
(λ (_x : M₀), _x * 0) = 0

To match `mul_one_eq_id`.

@[protected]
theorem function.injective.no_zero_divisors {M₀ : Type u_2} {M₀' : Type u_4} [has_mul M₀] [has_zero M₀] [has_mul M₀'] [has_zero M₀'] [no_zero_divisors M₀'] (f : M₀ → M₀') (hf : function.injective f) (zero : f 0 = 0) (mul : ∀ (x y : M₀), f (x * y) = f x * f y) :

Pushforward a `no_zero_divisors` instance along an injective function.

theorem eq_zero_of_mul_self_eq_zero {M₀ : Type u_2} [has_mul M₀] [has_zero M₀] [no_zero_divisors M₀] {a : M₀} (h : a * a = 0) :
a = 0
theorem mul_ne_zero {M₀ : Type u_2} [has_mul M₀] [has_zero M₀] [no_zero_divisors M₀] {a b : M₀} (ha : a 0) (hb : b 0) :
a * b 0
@[simp]
theorem mul_eq_zero {M₀ : Type u_2} [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_2} [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_2} [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_eq_zero_comm {M₀ : Type u_2} [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_2} [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_2} [mul_zero_class M₀] [no_zero_divisors M₀] {a : M₀} :
a * a = 0 a = 0
theorem zero_eq_mul_self {M₀ : Type u_2} [mul_zero_class M₀] [no_zero_divisors M₀] {a : M₀} :
0 = a * a a = 0
theorem mul_self_ne_zero {M₀ : Type u_2} [mul_zero_class M₀] [no_zero_divisors M₀] {a : M₀} :
a * a 0 a 0
theorem zero_ne_mul_self {M₀ : Type u_2} [mul_zero_class M₀] [no_zero_divisors M₀] {a : M₀} :
0 a * a a 0
@[protected, reducible]
def function.injective.mul_zero_one_class {M₀ : Type u_2} {M₀' : Type u_4} [has_mul M₀'] [has_zero M₀'] [has_one M₀'] (f : M₀' → M₀) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (a b : M₀'), f (a * b) = f a * f b) :

Pullback a `mul_zero_one_class` instance along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.mul_zero_one_class {M₀ : Type u_2} {M₀' : Type u_4} [has_mul M₀'] [has_zero M₀'] [has_one M₀'] (f : M₀ → M₀') (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (a b : M₀), f (a * b) = f a * f b) :

Pushforward a `mul_zero_one_class` instance along an surjective function. See note [reducible non-instances].

Equations
theorem eq_zero_of_zero_eq_one {M₀ : Type u_2} (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_2} (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
theorem subsingleton_iff_zero_eq_one {M₀ : Type u_2}  :
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_2}  :
0 = 1

Alias of the forward direction of `subsingleton_iff_zero_eq_one`.

theorem eq_of_zero_eq_one {M₀ : Type u_2} (h : 0 = 1) (a b : M₀) :
a = b
theorem zero_ne_one_or_forall_eq_0 {M₀ : Type u_2}  :
0 1 ∀ (a : M₀), a = 0

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

@[simp]
theorem zero_ne_one {M₀ : Type u_2} [nontrivial M₀] :
0 1

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

@[simp]
theorem one_ne_zero {M₀ : Type u_2} [nontrivial M₀] :
1 0
theorem ne_zero_of_eq_one {M₀ : Type u_2} [nontrivial M₀] {a : M₀} (h : a = 1) :
a 0
theorem left_ne_zero_of_mul_eq_one {M₀ : Type u_2} [nontrivial M₀] {a b : M₀} (h : a * b = 1) :
a 0
theorem right_ne_zero_of_mul_eq_one {M₀ : Type u_2} [nontrivial M₀] {a b : M₀} (h : a * b = 1) :
b 0
@[protected]
theorem pullback_nonzero {M₀ : Type u_2} {M₀' : Type u_4} [nontrivial M₀] [has_zero M₀'] [has_one M₀'] (f : M₀' → M₀) (zero : f 0 = 0) (one : f 1 = 1) :

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

@[protected, reducible]
def function.injective.semigroup_with_zero {M₀ : Type u_2} {M₀' : Type u_4} [has_zero M₀'] [has_mul M₀'] (f : M₀' → M₀) (hf : function.injective f) (zero : f 0 = 0) (mul : ∀ (x y : M₀'), f (x * y) = f x * f y) :

Pullback a `semigroup_with_zero` class along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.semigroup_with_zero {M₀ : Type u_2} {M₀' : Type u_4} [has_zero M₀'] [has_mul M₀'] (f : M₀ → M₀') (hf : function.surjective f) (zero : f 0 = 0) (mul : ∀ (x y : M₀), f (x * y) = f x * f y) :

Pushforward a `semigroup_with_zero` class along an surjective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.injective.monoid_with_zero {M₀ : Type u_2} {M₀' : Type u_4} [has_zero M₀'] [has_mul M₀'] [has_one M₀'] [has_pow M₀' ] [monoid_with_zero M₀] (f : M₀' → M₀) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : M₀'), f (x * y) = f x * f y) (npow : ∀ (x : M₀') (n : ), f (x ^ n) = f x ^ n) :

Pullback a `monoid_with_zero` class along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.monoid_with_zero {M₀ : Type u_2} {M₀' : Type u_4} [has_zero M₀'] [has_mul M₀'] [has_one M₀'] [has_pow M₀' ] [monoid_with_zero M₀] (f : M₀ → M₀') (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : M₀), f (x * y) = f x * f y) (npow : ∀ (x : M₀) (n : ), f (x ^ n) = f x ^ n) :

Pushforward a `monoid_with_zero` class along a surjective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.injective.comm_monoid_with_zero {M₀ : Type u_2} {M₀' : Type u_4} [has_zero M₀'] [has_mul M₀'] [has_one M₀'] [has_pow M₀' ] (f : M₀' → M₀) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : M₀'), f (x * y) = f x * f y) (npow : ∀ (x : M₀') (n : ), f (x ^ n) = f x ^ n) :

Pullback a `monoid_with_zero` class along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.comm_monoid_with_zero {M₀ : Type u_2} {M₀' : Type u_4} [has_zero M₀'] [has_mul M₀'] [has_one M₀'] [has_pow M₀' ] (f : M₀ → M₀') (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : M₀), f (x * y) = f x * f y) (npow : ∀ (x : M₀) (n : ), f (x ^ n) = f x ^ n) :

Pushforward a `monoid_with_zero` class along a surjective function. See note [reducible non-instances].

Equations
@[simp]
theorem units.ne_zero {M₀ : Type u_2} [monoid_with_zero M₀] [nontrivial M₀] (u : 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_2} [monoid_with_zero M₀] (u : M₀ˣ) {a : M₀} :
a * u = 0 a = 0
@[simp]
theorem units.mul_right_eq_zero {M₀ : Type u_2} [monoid_with_zero M₀] (u : M₀ˣ) {a : M₀} :
u * a = 0 a = 0
theorem is_unit.ne_zero {M₀ : Type u_2} [monoid_with_zero M₀] [nontrivial M₀] {a : M₀} (ha : is_unit a) :
a 0
theorem is_unit.mul_right_eq_zero {M₀ : Type u_2} [monoid_with_zero M₀] {a b : M₀} (ha : is_unit a) :
a * b = 0 b = 0
theorem is_unit.mul_left_eq_zero {M₀ : Type u_2} [monoid_with_zero M₀] {a b : M₀} (hb : is_unit b) :
a * b = 0 a = 0
@[simp]
theorem is_unit_zero_iff {M₀ : Type u_2} [monoid_with_zero M₀] :
0 = 1
@[simp]
theorem not_is_unit_zero {M₀ : Type u_2} [monoid_with_zero M₀] [nontrivial M₀] :
noncomputable def ring.inverse {M₀ : Type u_2} [monoid_with_zero M₀] :
M₀ → M₀

Introduce a function `inverse` on a monoid with zero `M₀`, which sends `x` to `x⁻¹` if `x` is invertible and to `0` otherwise. This definition is somewhat ad hoc, but one needs a fully (rather than partially) defined inverse function for some purposes, including for calculus.

Note that while this is in the `ring` namespace for brevity, it requires the weaker assumption `monoid_with_zero M₀` instead of `ring M₀`.

Equations
@[simp]
theorem ring.inverse_unit {M₀ : Type u_2} [monoid_with_zero M₀] (u : M₀ˣ) :

By definition, if `x` is invertible then `inverse x = x⁻¹`.

@[simp]
theorem ring.inverse_non_unit {M₀ : Type u_2} [monoid_with_zero M₀] (x : M₀) (h : ¬) :

By definition, if `x` is not invertible then `inverse x = 0`.

theorem ring.mul_inverse_cancel {M₀ : Type u_2} [monoid_with_zero M₀] (x : M₀) (h : is_unit x) :
= 1
theorem ring.inverse_mul_cancel {M₀ : Type u_2} [monoid_with_zero M₀] (x : M₀) (h : is_unit x) :
= 1
theorem ring.mul_inverse_cancel_right {M₀ : Type u_2} [monoid_with_zero M₀] (x y : M₀) (h : is_unit x) :
y * x * = y
theorem ring.inverse_mul_cancel_right {M₀ : Type u_2} [monoid_with_zero M₀] (x y : M₀) (h : is_unit x) :
* x = y
theorem ring.mul_inverse_cancel_left {M₀ : Type u_2} [monoid_with_zero M₀] (x y : M₀) (h : is_unit x) :
x * * y) = y
theorem ring.inverse_mul_cancel_left {M₀ : Type u_2} [monoid_with_zero M₀] (x y : M₀) (h : is_unit x) :
* (x * y) = y
@[simp]
theorem ring.inverse_one (M₀ : Type u_2) [monoid_with_zero M₀] :
@[simp]
theorem ring.inverse_zero (M₀ : Type u_2) [monoid_with_zero M₀] :
theorem ring.mul_inverse_rev' {M₀ : Type u_2} [monoid_with_zero M₀] {a b : M₀} (h : b) :
theorem ring.mul_inverse_rev {M₀ : Type u_1} (a b : M₀) :
theorem is_unit.ring_inverse {M₀ : Type u_2} [monoid_with_zero M₀] {a : M₀} :
@[simp]
theorem is_unit_ring_inverse {M₀ : Type u_2} [monoid_with_zero M₀] {a : M₀} :
theorem commute.ring_inverse_ring_inverse {M₀ : Type u_2} [monoid_with_zero M₀] {a b : M₀} (h : b) :
@[protected, instance]
theorem mul_left_inj' {M₀ : Type u_2} {a b c : M₀} (hc : c 0) :
a * c = b * c a = b
theorem mul_right_inj' {M₀ : Type u_2} {a b c : M₀} (ha : a 0) :
a * b = a * c b = c
@[simp]
theorem mul_eq_mul_right_iff {M₀ : Type u_2} {a b c : M₀} :
a * c = b * c a = b c = 0
@[simp]
theorem mul_eq_mul_left_iff {M₀ : Type u_2} {a b c : M₀} :
a * b = a * c b = c a = 0
theorem mul_right_eq_self₀ {M₀ : Type u_2} {a b : M₀} :
a * b = a b = 1 a = 0
theorem mul_left_eq_self₀ {M₀ : Type u_2} {a b : M₀} :
a * b = b a = 1 b = 0
@[protected, reducible]
def function.injective.cancel_monoid_with_zero {M₀ : Type u_2} {M₀' : Type u_4} [has_zero M₀'] [has_mul M₀'] [has_one M₀'] [has_pow M₀' ] (f : M₀' → M₀) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : M₀'), f (x * y) = f x * f y) (npow : ∀ (x : M₀') (n : ), f (x ^ n) = f x ^ n) :

Pullback a `monoid_with_zero` class along an injective function. See note [reducible non-instances].

Equations
theorem eq_zero_of_mul_eq_self_right {M₀ : Type u_2} {a b : M₀} (h₁ : b 1) (h₂ : a * b = a) :
a = 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_2} {a b : M₀} (h₁ : b 1) (h₂ : b * a = a) :
a = 0

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

@[protected, reducible]
def function.injective.cancel_comm_monoid_with_zero {M₀ : Type u_2} {M₀' : Type u_4} [has_zero M₀'] [has_mul M₀'] [has_one M₀'] [has_pow M₀' ] (f : M₀' → M₀) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : M₀'), f (x * y) = f x * f y) (npow : ∀ (x : M₀') (n : ), f (x ^ n) = f x ^ n) :

Pullback a `cancel_comm_monoid_with_zero` class along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.injective.group_with_zero {G₀ : Type u_3} {G₀' : Type u_5} [group_with_zero G₀] [has_zero G₀'] [has_mul G₀'] [has_one G₀'] [has_inv G₀'] [has_div G₀'] [has_pow G₀' ] [has_pow G₀' ] (f : G₀' → G₀) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : G₀'), f (x * y) = f x * f y) (inv : ∀ (x : G₀'), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : G₀'), f (x / y) = f x / f y) (npow : ∀ (x : G₀') (n : ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : G₀') (n : ), f (x ^ n) = f x ^ n) :

Pullback a `group_with_zero` class along an injective function. See note [reducible non-instances].

Equations
@[protected, reducible]
def function.surjective.group_with_zero {G₀ : Type u_3} {G₀' : Type u_5} [group_with_zero G₀] [has_zero G₀'] [has_mul G₀'] [has_one G₀'] [has_inv G₀'] [has_div G₀'] [has_pow G₀' ] [has_pow G₀' ] (h01 : 0 1) (f : G₀ → G₀') (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : G₀), f (x * y) = f x * f y) (inv : ∀ (x : G₀), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : G₀), f (x / y) = f x / f y) (npow : ∀ (x : G₀) (n : ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : G₀) (n : ), f (x ^ n) = f x ^ n) :

Pushforward a `group_with_zero` class along an surjective function. See note [reducible non-instances].

Equations
@[simp]
theorem mul_inv_cancel_right₀ {G₀ : Type u_3} [group_with_zero G₀] {b : G₀} (h : b 0) (a : G₀) :
a * b * b⁻¹ = a
@[simp]
theorem mul_inv_cancel_left₀ {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} (h : a 0) (b : G₀) :
a * (a⁻¹ * b) = b
theorem inv_ne_zero {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} (h : a 0) :
@[simp]
theorem inv_mul_cancel {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} (h : a 0) :
a⁻¹ * a = 1
theorem group_with_zero.mul_left_injective {G₀ : Type u_3} [group_with_zero G₀] {x : G₀} (h : x 0) :
function.injective (λ (y : G₀), x * y)
theorem group_with_zero.mul_right_injective {G₀ : Type u_3} [group_with_zero G₀] {x : G₀} (h : x 0) :
function.injective (λ (y : G₀), y * x)
@[simp]
theorem inv_mul_cancel_right₀ {G₀ : Type u_3} [group_with_zero G₀] {b : G₀} (h : b 0) (a : G₀) :
a * b⁻¹ * b = a
@[simp]
theorem inv_mul_cancel_left₀ {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} (h : a 0) (b : G₀) :
a⁻¹ * (a * b) = b
@[protected, instance]
def group_with_zero.to_division_monoid {G₀ : Type u_3} [group_with_zero G₀] :
Equations
def units.mk0 {G₀ : Type u_3} [group_with_zero G₀] (a : G₀) (ha : a 0) :
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.mk0_one {G₀ : Type u_3} [group_with_zero G₀] (h : 1 0 := one_ne_zero) :
h = 1
@[simp]
theorem units.coe_mk0 {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} (h : a 0) :
h) = a
@[simp]
theorem units.mk0_coe {G₀ : Type u_3} [group_with_zero G₀] (u : G₀ˣ) (h : u 0) :
h = u
@[simp]
theorem units.mul_inv' {G₀ : Type u_3} [group_with_zero G₀] (u : G₀ˣ) :
u * (u)⁻¹ = 1
@[simp]
theorem units.inv_mul' {G₀ : Type u_3} [group_with_zero G₀] (u : G₀ˣ) :
(u)⁻¹ * u = 1
@[simp]
theorem units.mk0_inj {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (ha : a 0) (hb : b 0) :
ha = hb a = b
theorem units.exists0 {G₀ : Type u_3} [group_with_zero G₀] {p : G₀ˣ → Prop} :
(∃ (g : G₀ˣ), p g) ∃ (g : G₀) (hg : g 0), p hg)

In a group with zero, an existential over a unit can be rewritten in terms of `units.mk0`.

theorem units.exists0' {G₀ : Type u_3} [group_with_zero G₀] {p : Π (g : G₀), g 0 → Prop} :
(∃ (g : G₀) (hg : g 0), p g hg) ∃ (g : G₀ˣ), p g _

An alternative version of `units.exists0`. This one is useful if Lean cannot figure out `p` when using `units.exists0` from right to left.

@[simp]
theorem units.exists_iff_ne_zero {G₀ : Type u_3} [group_with_zero G₀] {x : G₀} :
(∃ (u : G₀ˣ), u = x) x 0
theorem group_with_zero.eq_zero_or_unit {G₀ : Type u_3} [group_with_zero G₀] (a : G₀) :
a = 0 ∃ (u : G₀ˣ), a = u
@[simp]
theorem units.smul_mk0 {G₀ : Type u_3} [group_with_zero G₀] {α : Type u_1} [has_smul G₀ α] {g : G₀} (hg : g 0) (a : α) :
hg a = g a
theorem is_unit.mk0 {G₀ : Type u_3} [group_with_zero G₀] (x : G₀) (hx : x 0) :
theorem is_unit_iff_ne_zero {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} :
a 0
@[protected]
theorem ne.is_unit {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} :
a 0

Alias of the reverse direction of `is_unit_iff_ne_zero`.

@[protected, instance]
def group_with_zero.no_zero_divisors {G₀ : Type u_3} [group_with_zero G₀] :
@[simp]
theorem units.mk0_mul {G₀ : Type u_3} [group_with_zero G₀] (x y : G₀) (hxy : x * y 0) :
units.mk0 (x * y) hxy = _ * _
@[simp]
theorem div_self {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} (h : a 0) :
a / a = 1
theorem eq_mul_inv_iff_mul_eq₀ {G₀ : Type u_3} [group_with_zero G₀] {a b c : G₀} (hc : c 0) :
a = b * c⁻¹ a * c = b
theorem eq_inv_mul_iff_mul_eq₀ {G₀ : Type u_3} [group_with_zero G₀] {a b c : G₀} (hb : b 0) :
a = b⁻¹ * c b * a = c
theorem inv_mul_eq_iff_eq_mul₀ {G₀ : Type u_3} [group_with_zero G₀] {a b c : G₀} (ha : a 0) :
a⁻¹ * b = c b = a * c
theorem mul_inv_eq_iff_eq_mul₀ {G₀ : Type u_3} [group_with_zero G₀] {a b c : G₀} (hb : b 0) :
a * b⁻¹ = c a = c * b
theorem mul_inv_eq_one₀ {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (hb : b 0) :
a * b⁻¹ = 1 a = b
theorem inv_mul_eq_one₀ {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (ha : a 0) :
a⁻¹ * b = 1 a = b
theorem mul_eq_one_iff_eq_inv₀ {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (hb : b 0) :
a * b = 1 a = b⁻¹
theorem mul_eq_one_iff_inv_eq₀ {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (ha : a 0) :
a * b = 1 a⁻¹ = b
@[simp]
theorem div_mul_cancel {G₀ : Type u_3} [group_with_zero G₀] {b : G₀} (a : G₀) (h : b 0) :
a / b * b = a
@[simp]
theorem mul_div_cancel {G₀ : Type u_3} [group_with_zero G₀] {b : G₀} (a : G₀) (h : b 0) :
a * b / b = a
theorem mul_one_div_cancel {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} (h : a 0) :
a * (1 / a) = 1
theorem one_div_mul_cancel {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} (h : a 0) :
1 / a * a = 1
theorem div_left_inj' {G₀ : Type u_3} [group_with_zero G₀] {a b c : G₀} (hc : c 0) :
a / c = b / c a = b
theorem div_eq_iff {G₀ : Type u_3} [group_with_zero G₀] {a b c : G₀} (hb : b 0) :
a / b = c a = c * b
theorem eq_div_iff {G₀ : Type u_3} [group_with_zero G₀] {a b c : G₀} (hb : b 0) :
c = a / b c * b = a
theorem div_eq_iff_mul_eq {G₀ : Type u_3} [group_with_zero G₀] {a b c : G₀} (hb : b 0) :
a / b = c c * b = a
theorem eq_div_iff_mul_eq {G₀ : Type u_3} [group_with_zero G₀] {a b c : G₀} (hc : c 0) :
a = b / c a * c = b
theorem div_eq_of_eq_mul {G₀ : Type u_3} [group_with_zero G₀] {a b c : G₀} (hb : b 0) :
a = c * ba / b = c
theorem eq_div_of_mul_eq {G₀ : Type u_3} [group_with_zero G₀] {a b c : G₀} (hc : c 0) :
a * c = ba = b / c
theorem div_eq_one_iff_eq {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (hb : b 0) :
a / b = 1 a = b
theorem div_mul_left {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (hb : b 0) :
b / (a * b) = 1 / a
theorem mul_div_mul_right {G₀ : Type u_3} [group_with_zero G₀] {c : G₀} (a b : G₀) (hc : c 0) :
a * c / (b * c) = a / b
theorem mul_mul_div {G₀ : Type u_3} [group_with_zero G₀] {b : G₀} (a : G₀) (hb : b 0) :
a = a * b * (1 / b)
theorem div_div_div_cancel_right {G₀ : Type u_3} [group_with_zero G₀] {b c : G₀} (a : G₀) (hc : c 0) :
a / c / (b / c) = a / b
theorem div_mul_div_cancel {G₀ : Type u_3} [group_with_zero G₀] {b c : G₀} (a : G₀) (hc : c 0) :
a / c * (c / b) = a / b
@[simp]
theorem zero_div {G₀ : Type u_3} [group_with_zero G₀] (a : G₀) :
0 / a = 0
@[simp]
theorem div_zero {G₀ : Type u_3} [group_with_zero G₀] (a : G₀) :
a / 0 = 0
@[simp]
theorem mul_self_mul_inv {G₀ : Type u_3} [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_3} [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_3} [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_3} [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_3} [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 div_mul_cancel_of_imp {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (h : b = 0a = 0) :
a / b * b = a
theorem mul_div_cancel_of_imp {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (h : b = 0a = 0) :
a * b / b = a
@[simp]
theorem div_self_mul_self' {G₀ : Type u_3} [group_with_zero G₀] (a : G₀) :
a / (a * a) = a⁻¹
theorem one_div_ne_zero {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} (h : a 0) :
1 / a 0
@[simp]
theorem inv_eq_zero {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} :
a⁻¹ = 0 a = 0
@[simp]
theorem zero_eq_inv {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} :
0 = a⁻¹ 0 = a
@[simp]
theorem divp_mk0 {G₀ : Type u_3} [group_with_zero G₀] (a : G₀) {b : G₀} (hb : b 0) :
a /ₚ hb = a / b
theorem div_ne_zero {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (ha : a 0) (hb : b 0) :
a / b 0
@[simp]
theorem div_eq_zero_iff {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} :
a / b = 0 a = 0 b = 0
theorem div_ne_zero_iff {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} :
a / b 0 a 0 b 0
theorem ring.inverse_eq_inv {G₀ : Type u_3} [group_with_zero G₀] (a : G₀) :
@[simp]
theorem ring.inverse_eq_inv' {G₀ : Type u_3} [group_with_zero G₀] :
@[simp]
theorem div_div_self {G₀ : Type u_3} [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_3} [group_with_zero G₀] {a : G₀} (h : 1 / a 0) :
a 0
theorem eq_zero_of_one_div_eq_zero {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} (h : 1 / a = 0) :
a = 0
@[protected, instance]
Equations
@[protected, reducible]
def function.injective.comm_group_with_zero {G₀ : Type u_3} {G₀' : Type u_5} [has_zero G₀'] [has_mul G₀'] [has_one G₀'] [has_inv G₀'] [has_div G₀'] [has_pow G₀' ] [has_pow G₀' ] (f : G₀' → G₀) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : G₀'), f (x * y) = f x * f y) (inv : ∀ (x : G₀'), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : G₀'), f (x / y) = f x / f y) (npow : ∀ (x : G₀') (n : ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : G₀') (n : ), f (x ^ n) = f x ^ n) :

Pullback a `comm_group_with_zero` class along an injective function. See note [reducible non-instances].

Equations
@[protected]
def function.surjective.comm_group_with_zero {G₀ : Type u_3} {G₀' : Type u_5} [has_zero G₀'] [has_mul G₀'] [has_one G₀'] [has_inv G₀'] [has_div G₀'] [has_pow G₀' ] [has_pow G₀' ] (h01 : 0 1) (f : G₀ → G₀') (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : G₀), f (x * y) = f x * f y) (inv : ∀ (x : G₀), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : G₀), f (x / y) = f x / f y) (npow : ∀ (x : G₀) (n : ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : G₀) (n : ), f (x ^ n) = f x ^ n) :

Pushforward a `comm_group_with_zero` class along a surjective function.

Equations
theorem div_mul_right {G₀ : Type u_3} {a : G₀} (b : G₀) (ha : a 0) :
a / (a * b) = 1 / b
theorem mul_div_cancel_left_of_imp {G₀ : Type u_3} {a b : G₀} (h : a = 0b = 0) :
a * b / a = b
theorem mul_div_cancel_left {G₀ : Type u_3} {a : G₀} (b : G₀) (ha : a 0) :
a * b / a = b
theorem mul_div_cancel_of_imp' {G₀ : Type u_3} {a b : G₀} (h : b = 0a = 0) :
b * (a / b) = a
theorem mul_div_cancel' {G₀ : Type u_3} {b : G₀} (a : G₀) (hb : b 0) :
b * (a / b) = a
theorem mul_div_mul_left {G₀ : Type u_3} {c : G₀} (a b : G₀) (hc : c 0) :
c * a / (c * b) = a / b
theorem mul_eq_mul_of_div_eq_div {G₀ : Type u_3} (a : G₀) {b : G₀} (c : G₀) {d : G₀} (hb : b 0) (hd : d 0) (h : a / b = c / d) :
a * d = c * b
theorem div_eq_div_iff {G₀ : Type u_3} {a b c d : G₀} (hb : b 0) (hd : d 0) :
a / b = c / d a * d = c * b
theorem div_div_cancel' {G₀ : Type u_3} {a b : G₀} (ha : a 0) :
a / (a / b) = b
theorem div_helper {G₀ : Type u_3} {a : G₀} (b : G₀) (h : a 0) :
1 / (a * b) * a = 1 / b
@[simp]
theorem semiconj_by.zero_right {G₀ : Type u_3} [mul_zero_class G₀] (a : G₀) :
0 0
@[simp]
theorem semiconj_by.zero_left {G₀ : Type u_3} [mul_zero_class G₀] (x y : G₀) :
x y
@[simp]
theorem semiconj_by.inv_symm_left_iff₀ {G₀ : Type u_3} [group_with_zero G₀] {a x y : G₀} :
y y x
theorem semiconj_by.inv_symm_left₀ {G₀ : Type u_3} [group_with_zero G₀] {a x y : G₀} (h : x y) :
x
theorem semiconj_by.inv_right₀ {G₀ : Type u_3} [group_with_zero G₀] {a x y : G₀} (h : x y) :
@[simp]
theorem semiconj_by.inv_right_iff₀ {G₀ : Type u_3} [group_with_zero G₀] {a x y : G₀} :
y⁻¹ x y
theorem semiconj_by.div_right {G₀ : Type u_3} [group_with_zero G₀] {a x y x' y' : G₀} (h : x y) (h' : x' y') :
(x / x') (y / y')
@[simp]
theorem commute.zero_right {G₀ : Type u_3} [mul_zero_class G₀] (a : G₀) :
0
@[simp]
theorem commute.zero_left {G₀ : Type u_3} [mul_zero_class G₀] (a : G₀) :
a
@[simp]
theorem commute.inv_left_iff₀ {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} :
b b
theorem commute.inv_left₀ {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (h : b) :
b
@[simp]
theorem commute.inv_right_iff₀ {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} :
theorem commute.inv_right₀ {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (h : b) :
@[simp]
theorem commute.div_right {G₀ : Type u_3} [group_with_zero G₀] {a b c : G₀} (hab : b) (hac : c) :
(b / c)
@[simp]
theorem commute.div_left {G₀ : Type u_3} [group_with_zero G₀] {a b c : G₀} (hac : c) (hbc : c) :
commute (a / b) c
theorem map_ne_zero {M₀ : Type u_2} {G₀ : Type u_3} {F : Type u_6} [group_with_zero G₀] [monoid_with_zero M₀] [nontrivial M₀] [ M₀] (f : F) {a : G₀} :
f a 0 a 0
@[simp]
theorem map_eq_zero {M₀ : Type u_2} {G₀ : Type u_3} {F : Type u_6} [group_with_zero G₀] [monoid_with_zero M₀] [nontrivial M₀] [ M₀] (f : F) {a : G₀} :
f a = 0 a = 0
theorem eq_on_inv₀ {G₀ : Type u_3} {M₀' : Type u_4} {F' : Type u_7} [group_with_zero G₀] [monoid_with_zero M₀'] [ M₀'] {a : G₀} (f g : F') (h : f a = g a) :
@[simp]
theorem map_inv₀ {G₀ : Type u_3} {G₀' : Type u_5} {F : Type u_6} [group_with_zero G₀] [group_with_zero G₀'] [ G₀'] (f : F) (a : G₀) :

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

@[simp]
theorem map_div₀ {G₀ : Type u_3} {G₀' : Type u_5} {F : Type u_6} [group_with_zero G₀] [group_with_zero G₀'] [ G₀'] (f : F) (a b : G₀) :
f (a / b) = f a / f b
noncomputable def monoid_with_zero.inverse {M : Type u_1}  :

We define the inverse as a `monoid_with_zero_hom` by extending the inverse map by zero on non-units.

Equations
@[simp]
theorem monoid_with_zero.coe_inverse {M : Type u_1}  :
@[simp]
theorem monoid_with_zero.inverse_apply {M : Type u_1} (a : M) :
def inv_monoid_with_zero_hom {G₀ : Type u_1}  :
G₀ →*₀ G₀

Inversion on a commutative group with zero, considered as a monoid with zero homomorphism.

Equations
noncomputable def group_with_zero_of_is_unit_or_eq_zero {M : Type u_8} [nontrivial M] [hM : monoid_with_zero M] (h : ∀ (a : M), a = 0) :

Constructs a `group_with_zero` structure on a `monoid_with_zero` consisting only of units and 0.

Equations
noncomputable def comm_group_with_zero_of_is_unit_or_eq_zero {M : Type u_8} [nontrivial M] [hM : comm_monoid_with_zero M] (h : ∀ (a : M), a = 0) :

Constructs a `comm_group_with_zero` structure on a `comm_monoid_with_zero` consisting only of units and 0.

Equations

### Order dual #

@[protected, instance]
def order_dual.mul_zero_class {α : Type u_1} [h : mul_zero_class α] :
Equations
@[protected, instance]
def order_dual.mul_zero_one_class {α : Type u_1} [h : mul_zero_one_class α] :
Equations
@[protected, instance]
def order_dual.no_zero_divisors {α : Type u_1} [has_mul α] [has_zero α] [h : no_zero_divisors α] :
@[protected, instance]
def order_dual.semigroup_with_zero {α : Type u_1} [h : semigroup_with_zero α] :
Equations
@[protected, instance]
def order_dual.monoid_with_zero {α : Type u_1} [h : monoid_with_zero α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def order_dual.cancel_comm_monoid_with_zero {α : Type u_1}  :
Equations
@[protected, instance]
def order_dual.group_with_zero {α : Type u_1} [h : group_with_zero α] :
Equations
@[protected, instance]
def order_dual.comm_group_with_zero {α : Type u_1} [h : comm_group_with_zero α] :
Equations

### Lexicographic order #

@[protected, instance]
def lex.mul_zero_class {α : Type u_1} [h : mul_zero_class α] :
Equations
@[protected, instance]
def lex.mul_zero_one_class {α : Type u_1} [h : mul_zero_one_class α] :
Equations
@[protected, instance]
def lex.no_zero_divisors {α : Type u_1} [has_mul α] [has_zero α] [h : no_zero_divisors α] :
@[protected, instance]
def lex.semigroup_with_zero {α : Type u_1} [h : semigroup_with_zero α] :
Equations
@[protected, instance]
def lex.monoid_with_zero {α : Type u_1} [h : monoid_with_zero α] :
Equations
@[protected, instance]
def lex.cancel_monoid_with_zero {α : Type u_1} [h : cancel_monoid_with_zero α] :
Equations
@[protected, instance]
def lex.comm_monoid_with_zero {α : Type u_1} [h : comm_monoid_with_zero α] :
Equations
@[protected, instance]
def lex.cancel_comm_monoid_with_zero {α : Type u_1}  :
Equations
@[protected, instance]
def lex.group_with_zero {α : Type u_1} [h : group_with_zero α] :
Equations
@[protected, instance]
def lex.comm_group_with_zero {α : Type u_1} [h : comm_group_with_zero α] :
Equations