mathlib documentation

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:

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.

The simpset field_simps is used by the tactic field_simp to reduce an expression in a field to an expression of the form n / d where n and d are division-free.

@[protected]
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₀) (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]
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₀') (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_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₀) (h : b = 0) :
a * 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₀} (h : a * b 0) :
a 0 b 0
theorem mul_eq_zero_of_ne_zero_imp_eq_zero {M₀ : Type u_1} [mul_zero_class M₀] {a b : M₀} (h : a 0b = 0) :
a * b = 0
@[protected]
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₀') (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_1} [has_mul M₀] [has_zero M₀] [no_zero_divisors M₀] {a : M₀} (h : a * a = 0) :
a = 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₀} (ha : a 0) (hb : b 0) :
a * 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
@[protected]
def function.injective.mul_zero_one_class {M₀ : Type u_1} {M₀' : Type u_3} [mul_zero_one_class M₀] [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]
def function.surjective.mul_zero_one_class {M₀ : Type u_1} {M₀' : Type u_3} [mul_zero_one_class M₀] [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_1} [mul_zero_one_class 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} [mul_zero_one_class M₀] (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_1} [mul_zero_one_class 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 subsingleton_of_zero_eq_one {M₀ : Type u_1} [mul_zero_one_class M₀] :
0 = 1subsingleton M₀

Alias of subsingleton_iff_zero_eq_one.

theorem eq_of_zero_eq_one {M₀ : Type u_1} [mul_zero_one_class M₀] (h : 0 = 1) (a b : M₀) :
a = b
theorem zero_ne_one_or_forall_eq_0 {M₀ : Type u_1} [mul_zero_one_class M₀] :
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_1} [mul_zero_one_class 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} [mul_zero_one_class M₀] [nontrivial M₀] :
1 0
theorem ne_zero_of_eq_one {M₀ : Type u_1} [mul_zero_one_class M₀] [nontrivial M₀] {a : M₀} (h : a = 1) :
a 0
theorem left_ne_zero_of_mul_eq_one {M₀ : Type u_1} [mul_zero_one_class M₀] [nontrivial M₀] {a b : M₀} (h : a * b = 1) :
a 0
theorem right_ne_zero_of_mul_eq_one {M₀ : Type u_1} [mul_zero_one_class M₀] [nontrivial M₀] {a b : M₀} (h : a * b = 1) :
b 0
@[protected]
theorem pullback_nonzero {M₀ : Type u_1} {M₀' : Type u_3} [mul_zero_one_class M₀] [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]
def function.injective.semigroup_with_zero {M₀ : Type u_1} {M₀' : Type u_3} [has_zero M₀'] [has_mul M₀'] [semigroup_with_zero 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]
def function.surjective.semigroup_with_zero {M₀ : Type u_1} {M₀' : Type u_3} [semigroup_with_zero M₀] [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]
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₀) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : M₀'), f (x * y) = (f x) * f y) :

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

Equations
@[protected]
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₀') (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : M₀), f (x * y) = (f x) * f y) :

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

Equations
@[protected]
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₀) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : M₀'), f (x * y) = (f x) * f y) :

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

Equations
@[protected]
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₀') (hf : function.surjective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : M₀), f (x * y) = (f x) * f y) :

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

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₀} (ha : is_unit a) :
a 0
theorem is_unit.mul_right_eq_zero {M₀ : Type u_1} [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_1} [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_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₀] :
noncomputable def ring.inverse {M₀ : Type u_1} [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_1} [monoid_with_zero M₀] (u : units M₀) :

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

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

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

theorem ring.mul_inverse_cancel {M₀ : Type u_1} [monoid_with_zero M₀] (x : M₀) (h : is_unit x) :
theorem ring.inverse_mul_cancel {M₀ : Type u_1} [monoid_with_zero M₀] (x : M₀) (h : is_unit x) :
(ring.inverse x) * x = 1
theorem ring.mul_inverse_cancel_right {M₀ : Type u_1} [monoid_with_zero M₀] (x y : M₀) (h : is_unit x) :
(y * x) * ring.inverse x = y
theorem ring.inverse_mul_cancel_right {M₀ : Type u_1} [monoid_with_zero M₀] (x y : M₀) (h : is_unit x) :
(y * ring.inverse x) * x = y
theorem ring.mul_inverse_cancel_left {M₀ : Type u_1} [monoid_with_zero M₀] (x y : M₀) (h : is_unit x) :
x * (ring.inverse x) * y = y
theorem ring.inverse_mul_cancel_left {M₀ : Type u_1} [monoid_with_zero M₀] (x y : M₀) (h : is_unit x) :
(ring.inverse x) * x * y = y
@[simp]
theorem ring.inverse_one (M₀ : Type u_1) [monoid_with_zero M₀] :
@[simp]
theorem ring.inverse_zero (M₀ : Type u_1) [monoid_with_zero M₀] :
theorem ring.mul_inverse_rev' {M₀ : Type u_1} [monoid_with_zero M₀] {a b : M₀} (h : commute a b) :
theorem ring.mul_inverse_rev {M₀ : Type u_1} [comm_monoid_with_zero M₀] (a b : M₀) :
theorem is_unit.ring_inverse {M₀ : Type u_1} [monoid_with_zero M₀] {a : M₀} :
@[simp]
theorem is_unit_ring_inverse {M₀ : Type u_1} [monoid_with_zero M₀] {a : M₀} :
theorem commute.ring_inverse_ring_inverse {M₀ : Type u_1} [monoid_with_zero M₀] {a b : M₀} (h : commute a b) :
@[protected, instance]
theorem mul_left_inj' {M₀ : Type u_1} [cancel_monoid_with_zero M₀] {a b c : M₀} (hc : 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₀} (ha : 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
@[protected]
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₀) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (mul : ∀ (x y : M₀'), f (x * y) = (f x) * f y) :

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_1} [cancel_monoid_with_zero M₀] {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_1} [cancel_monoid_with_zero M₀] {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]
def function.injective.cancel_comm_monoid_with_zero {M₀ : Type u_1} {M₀' : Type u_3} [cancel_comm_monoid_with_zero M₀] [has_zero M₀'] [has_mul M₀'] [has_one 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) :

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

Equations
theorem division_def {G : Type u} [div_inv_monoid G] (a b : G) :
a / b = a * b⁻¹

Alias of div_eq_mul_inv.

@[protected]
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₀'] [has_div 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) :

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

Equations
@[protected]
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₀'] [has_div 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) :

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_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₀} (h : a 0) :
@[simp]
theorem inv_mul_cancel {G₀ : Type u_2} [group_with_zero G₀] {a : G₀} (h : a 0) :
a⁻¹ * a = 1
theorem group_with_zero.mul_left_injective {G₀ : Type u_2} [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_2} [group_with_zero G₀] {x : G₀} (h : x 0) :
function.injective (λ (y : G₀), y * x)
@[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₀} (h : a * b = 1) :
b = a⁻¹
theorem eq_inv_of_mul_left_eq_one {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} (h : a * b = 1) :
a = 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

This is the analogue of inv_eq_iff_inv_eq for group_with_zero. It could also be named inv_eq_iff_inv_eq'.

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

This is the analogue of eq_inv_iff_eq_inv for group_with_zero. It could also be named eq_inv_iff_eq_inv'.

@[simp]
theorem inv_eq_one₀ {G₀ : Type u_2} [group_with_zero G₀] {g : G₀} :
g⁻¹ = 1 g = 1
theorem eq_mul_inv_iff_mul_eq₀ {G₀ : Type u_2} [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_2} [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_2} [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_2} [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_2} [group_with_zero G₀] {a b : G₀} (hb : b 0) :
a * b⁻¹ = 1 a = b
theorem inv_mul_eq_one₀ {G₀ : Type u_2} [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_2} [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_2} [group_with_zero G₀] {a b : G₀} (ha : a 0) :
a * b = 1 a⁻¹ = b
def units.mk0 {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) (ha : a 0) :
units 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_2} [group_with_zero G₀] (h : 1 0 := one_ne_zero) :
units.mk0 1 h = 1
@[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, norm_cast]
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 group_with_zero.eq_zero_or_unit {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) :
a = 0 ∃ (u : units G₀), a = u
@[protected, instance]
def units.can_lift {G₀ : Type u_2} [group_with_zero G₀] :
can_lift G₀ (units G₀)
Equations
theorem is_unit.mk0 {G₀ : Type u_2} [group_with_zero G₀] (x : G₀) (hx : x 0) :
theorem is_unit_iff_ne_zero {G₀ : Type u_2} [group_with_zero G₀] {x : G₀} :
@[protected, instance]
@[simp]
theorem units.mk0_mul {G₀ : Type u_2} [group_with_zero G₀] (x y : G₀) (hxy : x * y 0) :
units.mk0 (x * y) hxy = (units.mk0 x _) * units.mk0 y _
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₀} (h : a 0) :
a / a = 1
@[simp]
theorem div_one {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) :
a / 1 = 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₀} (h : b 0) :
(a / b) * b = a
theorem div_mul_cancel_of_imp {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} (h : b = 0a = 0) :
(a / b) * b = a
@[simp]
theorem mul_div_cancel {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) {b : G₀} (h : b 0) :
a * b / b = a
theorem mul_div_cancel_of_imp {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} (h : b = 0a = 0) :
a * b / b = a
@[simp]
theorem div_self_mul_self' {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) :
a / a * a = a⁻¹
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₀} (h : a 0) :
a * (1 / a) = 1
theorem one_div_mul_cancel {G₀ : Type u_2} [group_with_zero G₀] {a : G₀} (h : 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₀} (h : a 0) :
1 / a 0
theorem eq_one_div_of_mul_eq_one {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} (h : a * b = 1) :
b = 1 / a
theorem eq_one_div_of_mul_eq_one_left {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} (h : b * a = 1) :
b = 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₀} (h : 1 / a = 1 / b) :
a = 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₀} (ha : a 0) (hb : b 0) :
a / 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₀} (hc : 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₀} (hb : 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₀} (hc : 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₀} (h : y = z * x) :
y / x = z
theorem eq_div_of_mul_eq {G₀ : Type u_2} [group_with_zero G₀] {x : G₀} (hx : x 0) {y z : G₀} (h : z * x = y) :
z = y / x
theorem eq_of_div_eq_one {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} (h : a / b = 1) :
a = b
theorem div_eq_one_iff_eq {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} (hb : b 0) :
a / b = 1 a = b
theorem div_mul_left {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} (hb : b 0) :
b / a * b = 1 / a
theorem mul_div_mul_right {G₀ : Type u_2} [group_with_zero G₀] (a b : G₀) {c : G₀} (hc : c 0) :
a * c / b * c = a / b
theorem mul_mul_div {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) {b : G₀} (hb : b 0) :
a = (a * b) * (1 / b)
theorem ring.inverse_eq_inv {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) :
@[simp]
theorem ring.inverse_eq_inv' {G₀ : Type u_2} [group_with_zero G₀] :
theorem div_div_eq_mul_div {G₀ : Type u_2} [group_with_zero G₀] (a b c : G₀) :
a / (b / c) = a * c / b
@[simp]
theorem div_div_self {G₀ : Type u_2} [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} [group_with_zero G₀] {a : G₀} (h : 1 / a 0) :
a 0
theorem eq_zero_of_one_div_eq_zero {G₀ : Type u_2} [group_with_zero G₀] {a : G₀} (h : 1 / a = 0) :
a = 0
theorem div_div_div_cancel_right {G₀ : Type u_2} [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_2} [group_with_zero G₀] {b c : G₀} (a : G₀) (hc : c 0) :
(a / c) * (c / b) = a / b
theorem eq_div_iff {G₀ : Type u_2} [group_with_zero G₀] {a b c : G₀} (hb : b 0) :
c = a / b c * b = a
theorem div_eq_iff {G₀ : Type u_2} [group_with_zero G₀] {a b c : G₀} (hb : b 0) :
a / b = c a = c * b
@[protected]
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₀'] [has_div 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) :

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_2} {G₀' : Type u_4} [comm_group_with_zero G₀] [has_zero G₀'] [has_mul G₀'] [has_one G₀'] [has_inv G₀'] [has_div 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) :

Pushforward a comm_group_with_zero class along a 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₀) (ha : a 0) :
a / a * b = 1 / b
theorem mul_div_cancel_left_of_imp {G₀ : Type u_2} [comm_group_with_zero G₀] {a b : G₀} (h : 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₀) (ha : a 0) :
a * b / a = b
theorem mul_div_cancel_of_imp' {G₀ : Type u_2} [comm_group_with_zero G₀] {a b : G₀} (h : b = 0a = 0) :
b * (a / b) = a
theorem mul_div_cancel' {G₀ : Type u_2} [comm_group_with_zero G₀] (a : G₀) {b : G₀} (hb : b 0) :
b * (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₀} (hc : c 0) :
c * 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₀} (hb : b 0) (hd : d 0) (h : a / b = c / d) :
a * d = 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)
theorem div_helper {G₀ : Type u_2} [comm_group_with_zero G₀] {a : G₀} (b : G₀) (h : 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_eq_div_iff {G₀ : Type u_2} [comm_group_with_zero G₀] {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_2} [comm_group_with_zero G₀] {a b : G₀} (ha : a 0) :
a / (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₀} (h : semiconj_by a x y) :
theorem semiconj_by.inv_right₀ {G₀ : Type u_2} [group_with_zero G₀] {a x y : G₀} (h : semiconj_by a x y) :
@[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₀} (h : semiconj_by a x y) (h' : semiconj_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₀} (h : commute 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₀} (h : commute a b) :
theorem commute.inv_inv₀ {G₀ : Type u_2} [group_with_zero G₀] {a b : G₀} (h : commute a b) :
@[simp]
theorem commute.div_right {G₀ : Type u_2} [group_with_zero G₀] {a b c : G₀} (hab : commute a b) (hac : commute a c) :
commute a (b / c)
@[simp]
theorem commute.div_left {G₀ : Type u_2} [group_with_zero G₀] {a b c : G₀} (hac : commute a c) (hbc : commute b c) :
commute (a / b) c
theorem monoid_with_zero_hom.map_ne_zero {M₀ : Type u_1} {G₀ : Type u_2} [group_with_zero G₀] [monoid_with_zero M₀] [nontrivial M₀] (f : monoid_with_zero_hom G₀ M₀) {a : G₀} :
f a 0 a 0
@[simp]
theorem monoid_with_zero_hom.map_eq_zero {M₀ : Type u_1} {G₀ : Type u_2} [group_with_zero G₀] [monoid_with_zero M₀] [nontrivial M₀] (f : monoid_with_zero_hom G₀ M₀) {a : G₀} :
f a = 0 a = 0
@[simp]
theorem monoid_with_zero_hom.map_inv {G₀ : Type u_2} {G₀' : Type u_4} [group_with_zero G₀] [group_with_zero G₀'] (f : monoid_with_zero_hom G₀ G₀') (a : G₀) :

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

@[simp]
theorem monoid_with_zero_hom.map_div {G₀ : Type u_2} {G₀' : Type u_4} [group_with_zero G₀] [group_with_zero G₀'] (f : monoid_with_zero_hom G₀ G₀') (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) :
@[simp]
theorem monoid_with_zero_hom.map_units_inv {M : Type u_1} {G₀ : Type u_2} [monoid_with_zero M] [group_with_zero G₀] (f : monoid_with_zero_hom M G₀) (u : units M) :
noncomputable def group_with_zero_of_is_unit_or_eq_zero {M : Type u_5} [nontrivial M] [hM : monoid_with_zero M] (h : ∀ (a : M), is_unit a a = 0) :

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

Equations