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.

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

To match one_mul_eq_id.

theorem mul_zero_eq_const {M₀ : Type u_2} [mul_zero_class M₀] :
(λ (_x : M₀), _x * 0) = function.const M₀ 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} [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, reducible]
def function.surjective.mul_zero_one_class {M₀ : Type u_2} {M₀' : Type u_4} [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_2} [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_2} [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_2} [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_2} [mul_zero_one_class M₀] :
0 = 1subsingleton M₀

Alias of the forward direction of subsingleton_iff_zero_eq_one.

theorem eq_of_zero_eq_one {M₀ : Type u_2} [mul_zero_one_class M₀] (h : 0 = 1) (a b : M₀) :
a = b
theorem zero_ne_one_or_forall_eq_0 {M₀ : Type u_2} [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_2} [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_2} [mul_zero_one_class M₀] [nontrivial M₀] :
1 0
theorem ne_zero_of_eq_one {M₀ : Type u_2} [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_2} [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_2} [mul_zero_one_class M₀] [nontrivial M₀] {a b : M₀} (h : a * b = 1) :
b 0
@[protected]
theorem pullback_nonzero {M₀ : Type u_2} {M₀' : Type u_4} [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, reducible]
def function.injective.semigroup_with_zero {M₀ : Type u_2} {M₀' : Type u_4} [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, reducible]
def function.surjective.semigroup_with_zero {M₀ : Type u_2} {M₀' : Type u_4} [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, 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₀' ] [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) (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₀' ] [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) (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₀] :
is_unit 0 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 : ¬is_unit x) :

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) :
theorem ring.inverse_mul_cancel {M₀ : Type u_2} [monoid_with_zero M₀] (x : M₀) (h : is_unit x) :
theorem ring.mul_inverse_cancel_right {M₀ : Type u_2} [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_2} [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_2} [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_2} [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_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 : 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_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 : commute a b) :
@[protected, instance]
theorem mul_left_inj' {M₀ : Type u_2} [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_2} [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_2} [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_2} [cancel_monoid_with_zero M₀] {a b c : M₀} :
a * b = a * c b = c a = 0
theorem mul_right_eq_self₀ {M₀ : Type u_2} [cancel_monoid_with_zero M₀] {a b : M₀} :
a * b = a b = 1 a = 0
theorem mul_left_eq_self₀ {M₀ : Type u_2} [cancel_monoid_with_zero M₀] {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} [cancel_monoid_with_zero M₀] [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} [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_2} [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, reducible]
def function.injective.cancel_comm_monoid_with_zero {M₀ : Type u_2} {M₀' : Type u_4} [cancel_comm_monoid_with_zero M₀] [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
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) :
units.mk0 1 h = 1
@[simp]
theorem units.coe_mk0 {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} (h : a 0) :
(units.mk0 a h) = a
@[simp]
theorem units.mk0_coe {G₀ : Type u_3} [group_with_zero G₀] (u : G₀ˣ) (h : u 0) :
@[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) :
units.mk0 a ha = units.mk0 b 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 (units.mk0 g 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 : α) :
units.mk0 g 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₀} :
@[protected]
theorem ne.is_unit {G₀ : Type u_3} [group_with_zero G₀] {a : G₀} :
a 0is_unit a

Alias of the reverse direction of is_unit_iff_ne_zero.

@[protected, instance]
@[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 = units.mk0 x _ * units.mk0 y _
@[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 /ₚ units.mk0 b 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, reducible]
def function.injective.comm_group_with_zero {G₀ : Type u_3} {G₀' : Type u_5} [comm_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 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} [comm_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 comm_group_with_zero class along a surjective function.

Equations
theorem div_mul_right {G₀ : Type u_3} [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_3} [comm_group_with_zero G₀] {a b : G₀} (h : a = 0b = 0) :
a * b / a = b
theorem mul_div_cancel_left {G₀ : Type u_3} [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_3} [comm_group_with_zero G₀] {a b : G₀} (h : b = 0a = 0) :
b * (a / b) = a
theorem mul_div_cancel' {G₀ : Type u_3} [comm_group_with_zero G₀] {b : G₀} (a : G₀) (hb : b 0) :
b * (a / b) = a
theorem mul_div_mul_left {G₀ : Type u_3} [comm_group_with_zero G₀] {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} [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_eq_div_iff {G₀ : Type u_3} [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_3} [comm_group_with_zero G₀] {a b : G₀} (ha : a 0) :
a / (a / b) = b
theorem div_helper {G₀ : Type u_3} [comm_group_with_zero G₀] {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₀) :
@[simp]
theorem semiconj_by.zero_left {G₀ : Type u_3} [mul_zero_class G₀] (x y : G₀) :
@[simp]
theorem semiconj_by.inv_symm_left_iff₀ {G₀ : Type u_3} [group_with_zero G₀] {a x y : G₀} :
theorem semiconj_by.inv_symm_left₀ {G₀ : Type u_3} [group_with_zero G₀] {a x y : G₀} (h : semiconj_by a x y) :
theorem semiconj_by.inv_right₀ {G₀ : Type u_3} [group_with_zero G₀] {a x y : G₀} (h : semiconj_by a x y) :
@[simp]
theorem semiconj_by.inv_right_iff₀ {G₀ : Type u_3} [group_with_zero G₀] {a x y : G₀} :
theorem semiconj_by.div_right {G₀ : Type u_3} [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_3} [mul_zero_class G₀] (a : G₀) :
@[simp]
theorem commute.zero_left {G₀ : Type u_3} [mul_zero_class G₀] (a : G₀) :
@[simp]
theorem commute.inv_left_iff₀ {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} :
theorem commute.inv_left₀ {G₀ : Type u_3} [group_with_zero G₀] {a b : G₀} (h : commute a 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 : commute a b) :
@[simp]
theorem commute.div_right {G₀ : Type u_3} [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_3} [group_with_zero G₀] {a b c : G₀} (hac : commute a c) (hbc : commute b 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₀] [monoid_with_zero_hom_class F G₀ 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₀] [monoid_with_zero_hom_class F G₀ 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₀'] [monoid_with_zero_hom_class F' G₀ 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₀'] [monoid_with_zero_hom_class F 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₀'] [monoid_with_zero_hom_class F G₀ G₀'] (f : F) (a b : G₀) :
f (a / b) = f a / f b
noncomputable def monoid_with_zero.inverse {M : Type u_1} [comm_monoid_with_zero M] :

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

Equations
def inv_monoid_with_zero_hom {G₀ : Type u_1} [comm_group_with_zero G₀] :
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), is_unit a a = 0) :

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

Equations

Order dual #

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
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]
Equations
@[protected, instance]
def lex.monoid_with_zero {α : Type u_1} [h : monoid_with_zero α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def lex.group_with_zero {α : Type u_1} [h : group_with_zero α] :
Equations
@[protected, instance]
Equations