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]
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) :
mul_zero_class M₀'
Pullback a mul_zero_class instance along an injective function.
See note [reducible non-instances].
Equations
- function.injective.mul_zero_class f hf zero mul = {mul := has_mul.mul _inst_2, zero := 0, zero_mul := _, mul_zero := _}
@[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) :
mul_zero_class M₀'
Pushforward a mul_zero_class instance along an surjective function.
See note [reducible non-instances].
Equations
- function.surjective.mul_zero_class f hf zero mul = {mul := has_mul.mul _inst_2, zero := 0, zero_mul := _, mul_zero := _}
theorem
mul_eq_zero_of_ne_zero_imp_eq_zero
{M₀ : Type u_1}
[mul_zero_class M₀]
{a b : M₀}
(h : a ≠ 0 → b = 0) :
To match one_mul_eq_id.
theorem
mul_zero_eq_const
{M₀ : Type u_1}
[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_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]
If α has no zero divisors, then the product of two elements equals zero iff one of them
equals zero.
@[simp]
If α has no zero divisors, then the product of two elements equals zero iff one of them
equals zero.
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) :
If α has no zero divisors, then for elements a, b : α, a * b equals zero iff so is
b * a.
If α has no zero divisors, then for elements a, b : α, a * b is nonzero iff so is
b * a.
@[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
- function.injective.mul_zero_one_class f hf zero one mul = {one := mul_one_class.one (function.injective.mul_one_class f hf one mul), mul := mul_zero_class.mul (function.injective.mul_zero_class f hf zero mul), one_mul := _, mul_one := _, zero := mul_zero_class.zero (function.injective.mul_zero_class f hf zero mul), zero_mul := _, mul_zero := _}
@[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
- function.surjective.mul_zero_one_class f hf zero one mul = {one := mul_one_class.one (function.surjective.mul_one_class f hf one mul), mul := mul_zero_class.mul (function.surjective.mul_zero_class f hf zero mul), one_mul := _, mul_one := _, zero := mul_zero_class.zero (function.surjective.mul_zero_class f hf zero mul), zero_mul := _, mul_zero := _}
In a monoid with zero, if zero equals one, then zero is the only element.
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
- unique_of_zero_eq_one h = {to_inhabited := {default := 0}, uniq := _}
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 = 1 → subsingleton M₀
Alias of subsingleton_iff_zero_eq_one.
In a monoid with zero, either zero and one are nonequal, or zero is the only element.
@[simp]
In a nontrivial monoid with zero, zero and one are different.
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) :
nontrivial M₀'
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
- function.injective.semigroup_with_zero f hf zero mul = {mul := mul_zero_class.mul (function.injective.mul_zero_class f hf zero mul), mul_assoc := _, zero := mul_zero_class.zero (function.injective.mul_zero_class f hf zero mul), zero_mul := _, mul_zero := _}
@[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
- function.surjective.semigroup_with_zero f hf zero mul = {mul := mul_zero_class.mul (function.surjective.mul_zero_class f hf zero mul), mul_assoc := _, zero := mul_zero_class.zero (function.surjective.mul_zero_class f hf zero mul), zero_mul := _, mul_zero := _}
@[protected]
def
function.injective.monoid_with_zero
{M₀ : Type u_1}
{M₀' : Type u_3}
[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) :
monoid_with_zero M₀'
Pullback a monoid_with_zero class along an injective function.
See note [reducible non-instances].
Equations
- function.injective.monoid_with_zero f hf zero one mul npow = {mul := monoid.mul (function.injective.monoid f hf one mul npow), mul_assoc := _, one := monoid.one (function.injective.monoid f hf one mul npow), one_mul := _, mul_one := _, npow := monoid.npow (function.injective.monoid f hf one mul npow), npow_zero' := _, npow_succ' := _, zero := mul_zero_class.zero (function.injective.mul_zero_class f hf zero mul), zero_mul := _, mul_zero := _}
@[protected]
def
function.surjective.monoid_with_zero
{M₀ : Type u_1}
{M₀' : Type u_3}
[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) :
monoid_with_zero M₀'
Pushforward a monoid_with_zero class along a surjective function.
See note [reducible non-instances].
Equations
- function.surjective.monoid_with_zero f hf zero one mul npow = {mul := monoid.mul (function.surjective.monoid f hf one mul npow), mul_assoc := _, one := monoid.one (function.surjective.monoid f hf one mul npow), one_mul := _, mul_one := _, npow := monoid.npow (function.surjective.monoid f hf one mul npow), npow_zero' := _, npow_succ' := _, zero := mul_zero_class.zero (function.surjective.mul_zero_class f hf zero mul), zero_mul := _, mul_zero := _}
@[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₀']
[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
- function.injective.comm_monoid_with_zero f hf zero one mul npow = {mul := comm_monoid.mul (function.injective.comm_monoid f hf one mul npow), mul_assoc := _, one := comm_monoid.one (function.injective.comm_monoid f hf one mul npow), one_mul := _, mul_one := _, npow := comm_monoid.npow (function.injective.comm_monoid f hf one mul npow), npow_zero' := _, npow_succ' := _, mul_comm := _, zero := mul_zero_class.zero (function.injective.mul_zero_class f hf zero mul), zero_mul := _, mul_zero := _}
@[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₀']
[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
- function.surjective.comm_monoid_with_zero f hf zero one mul npow = {mul := comm_monoid.mul (function.surjective.comm_monoid f hf one mul npow), mul_assoc := _, one := comm_monoid.one (function.surjective.comm_monoid f hf one mul npow), one_mul := _, mul_one := _, npow := comm_monoid.npow (function.surjective.comm_monoid f hf one mul npow), npow_zero' := _, npow_succ' := _, mul_comm := _, zero := mul_zero_class.zero (function.surjective.mul_zero_class f hf zero mul), zero_mul := _, mul_zero := _}
@[simp]
An element of the unit group of a nonzero monoid with zero represented as an element of the monoid is nonzero.
@[simp]
@[simp]
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) :
theorem
is_unit.mul_left_eq_zero
{M₀ : Type u_1}
[monoid_with_zero M₀]
{a b : M₀}
(hb : is_unit b) :
@[simp]
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₀.
@[simp]
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) :
ring.inverse x = 0
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) :
x * ring.inverse x = 1
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
theorem
ring.mul_inverse_rev'
{M₀ : Type u_1}
[monoid_with_zero M₀]
{a b : M₀}
(h : commute a b) :
ring.inverse (a * b) = (ring.inverse b) * ring.inverse a
theorem
ring.mul_inverse_rev
{M₀ : Type u_1}
[comm_monoid_with_zero M₀]
(a b : M₀) :
ring.inverse (a * b) = (ring.inverse b) * ring.inverse a
theorem
is_unit.ring_inverse
{M₀ : Type u_1}
[monoid_with_zero M₀]
{a : M₀} :
is_unit a → is_unit (ring.inverse a)
@[simp]
theorem
is_unit_ring_inverse
{M₀ : Type u_1}
[monoid_with_zero M₀]
{a : M₀} :
is_unit (ring.inverse a) ↔ is_unit a
theorem
commute.ring_inverse_ring_inverse
{M₀ : Type u_1}
[monoid_with_zero M₀]
{a b : M₀}
(h : commute a b) :
commute (ring.inverse a) (ring.inverse b)
@[protected, instance]
@[simp]
@[simp]
@[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₀']
[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
- function.injective.cancel_monoid_with_zero f hf zero one mul npow = {mul := monoid.mul (function.injective.monoid f hf one mul npow), mul_assoc := _, one := monoid.one (function.injective.monoid f hf one mul npow), one_mul := _, mul_one := _, npow := monoid.npow (function.injective.monoid f hf one mul npow), npow_zero' := _, npow_succ' := _, zero := mul_zero_class.zero (function.injective.mul_zero_class f hf zero mul), zero_mul := _, mul_zero := _, mul_left_cancel_of_ne_zero := _, mul_right_cancel_of_ne_zero := _}
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₀']
[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
- function.injective.cancel_comm_monoid_with_zero f hf zero one mul npow = {mul := comm_monoid_with_zero.mul (function.injective.comm_monoid_with_zero f hf zero one mul npow), mul_assoc := _, one := comm_monoid_with_zero.one (function.injective.comm_monoid_with_zero f hf zero one mul npow), one_mul := _, mul_one := _, npow := comm_monoid_with_zero.npow (function.injective.comm_monoid_with_zero f hf zero one mul npow), npow_zero' := _, npow_succ' := _, mul_comm := _, zero := comm_monoid_with_zero.zero (function.injective.comm_monoid_with_zero f hf zero one mul npow), zero_mul := _, mul_zero := _, mul_left_cancel_of_ne_zero := _, mul_right_cancel_of_ne_zero := _}
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₀']
[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) :
group_with_zero G₀'
Pullback a group_with_zero class along an injective function.
See note [reducible non-instances].
Equations
- function.injective.group_with_zero f hf zero one mul inv div npow zpow = {mul := monoid_with_zero.mul (function.injective.monoid_with_zero f hf zero one mul npow), mul_assoc := _, one := monoid_with_zero.one (function.injective.monoid_with_zero f hf zero one mul npow), one_mul := _, mul_one := _, npow := monoid_with_zero.npow (function.injective.monoid_with_zero f hf zero one mul npow), npow_zero' := _, npow_succ' := _, zero := monoid_with_zero.zero (function.injective.monoid_with_zero f hf zero one mul npow), zero_mul := _, mul_zero := _, inv := div_inv_monoid.inv (function.injective.div_inv_monoid f hf one mul inv div npow zpow), div := div_inv_monoid.div (function.injective.div_inv_monoid f hf one mul inv div npow zpow), div_eq_mul_inv := _, zpow := div_inv_monoid.zpow (function.injective.div_inv_monoid f hf one mul inv div npow zpow), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}
@[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₀']
[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) :
group_with_zero G₀'
Pushforward a group_with_zero class along an surjective function.
See note [reducible non-instances].
Equations
- function.surjective.group_with_zero h01 f hf zero one mul inv div npow zpow = {mul := monoid_with_zero.mul (function.surjective.monoid_with_zero f hf zero one mul npow), mul_assoc := _, one := monoid_with_zero.one (function.surjective.monoid_with_zero f hf zero one mul npow), one_mul := _, mul_one := _, npow := monoid_with_zero.npow (function.surjective.monoid_with_zero f hf zero one mul npow), npow_zero' := _, npow_succ' := _, zero := monoid_with_zero.zero (function.surjective.monoid_with_zero f hf zero one mul npow), zero_mul := _, mul_zero := _, inv := div_inv_monoid.inv (function.surjective.div_inv_monoid f hf one mul inv div npow zpow), div := div_inv_monoid.div (function.surjective.div_inv_monoid f hf one mul inv div npow zpow), div_eq_mul_inv := _, zpow := div_inv_monoid.zpow (function.surjective.div_inv_monoid f hf one mul inv div npow zpow), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}
@[simp]
@[simp]
@[simp]
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]
@[simp]
@[protected, instance]
Equations
@[simp]
Multiplying a by itself and then by its inverse results in a
(whether or not a is zero).
@[simp]
Multiplying a by its inverse and then by itself results in a
(whether or not a is zero).
@[simp]
Multiplying a⁻¹ by a twice results in a (whether or not a
is zero).
@[simp]
Multiplying a by itself and then dividing by itself results in
a (whether or not a is zero).
@[simp]
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) :
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.
@[simp]
@[simp]
@[simp]
@[simp, norm_cast]
@[simp]
@[simp]
@[simp]
In a group with zero, an existential over a unit can be rewritten in terms of units.mk0.
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]
@[protected, instance]
@[protected, instance]
Equations
- group_with_zero.cancel_monoid_with_zero = {mul := group_with_zero.mul _inst_1, mul_assoc := _, one := group_with_zero.one _inst_1, one_mul := _, mul_one := _, npow := group_with_zero.npow _inst_1, npow_zero' := _, npow_succ' := _, zero := group_with_zero.zero _inst_1, zero_mul := _, mul_zero := _, mul_left_cancel_of_ne_zero := _, mul_right_cancel_of_ne_zero := _}
@[simp]
@[simp]
@[simp]
theorem
eq_one_div_of_mul_eq_one_left
{G₀ : Type u_2}
[group_with_zero G₀]
{a b : G₀}
(h : b * a = 1) :
@[simp]
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
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) :
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) :
@[simp]
@[simp]
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) :
@[protected, instance]
Equations
- comm_group_with_zero.cancel_comm_monoid_with_zero = {mul := cancel_monoid_with_zero.mul group_with_zero.cancel_monoid_with_zero, mul_assoc := _, one := cancel_monoid_with_zero.one group_with_zero.cancel_monoid_with_zero, one_mul := _, mul_one := _, npow := cancel_monoid_with_zero.npow group_with_zero.cancel_monoid_with_zero, npow_zero' := _, npow_succ' := _, mul_comm := _, zero := cancel_monoid_with_zero.zero group_with_zero.cancel_monoid_with_zero, zero_mul := _, mul_zero := _, mul_left_cancel_of_ne_zero := _, mul_right_cancel_of_ne_zero := _}
@[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₀']
[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
- function.injective.comm_group_with_zero f hf zero one mul inv div npow zpow = {mul := group_with_zero.mul (function.injective.group_with_zero f hf zero one mul inv div npow zpow), mul_assoc := _, one := group_with_zero.one (function.injective.group_with_zero f hf zero one mul inv div npow zpow), one_mul := _, mul_one := _, npow := group_with_zero.npow (function.injective.group_with_zero f hf zero one mul inv div npow zpow), npow_zero' := _, npow_succ' := _, mul_comm := _, zero := group_with_zero.zero (function.injective.group_with_zero f hf zero one mul inv div npow zpow), zero_mul := _, mul_zero := _, inv := group_with_zero.inv (function.injective.group_with_zero f hf zero one mul inv div npow zpow), div := group_with_zero.div (function.injective.group_with_zero f hf zero one mul inv div npow zpow), div_eq_mul_inv := _, zpow := group_with_zero.zpow (function.injective.group_with_zero f hf zero one mul inv div npow zpow), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}
@[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₀']
[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
- function.surjective.comm_group_with_zero h01 f hf zero one mul inv div npow zpow = {mul := group_with_zero.mul (function.surjective.group_with_zero h01 f hf zero one mul inv div npow zpow), mul_assoc := _, one := group_with_zero.one (function.surjective.group_with_zero h01 f hf zero one mul inv div npow zpow), one_mul := _, mul_one := _, npow := group_with_zero.npow (function.surjective.group_with_zero h01 f hf zero one mul inv div npow zpow), npow_zero' := _, npow_succ' := _, mul_comm := _, zero := group_with_zero.zero (function.surjective.group_with_zero h01 f hf zero one mul inv div npow zpow), zero_mul := _, mul_zero := _, inv := group_with_zero.inv (function.surjective.group_with_zero h01 f hf zero one mul inv div npow zpow), div := group_with_zero.div (function.surjective.group_with_zero h01 f hf zero one mul inv div npow zpow), div_eq_mul_inv := _, zpow := group_with_zero.zpow (function.surjective.group_with_zero h01 f hf zero one mul inv div npow zpow), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}
theorem
mul_div_cancel_left_of_imp
{G₀ : Type u_2}
[comm_group_with_zero G₀]
{a b : G₀}
(h : a = 0 → b = 0) :
theorem
mul_div_cancel_left
{G₀ : Type u_2}
[comm_group_with_zero G₀]
{a : G₀}
(b : G₀)
(ha : a ≠ 0) :
theorem
mul_div_cancel_of_imp'
{G₀ : Type u_2}
[comm_group_with_zero G₀]
{a b : G₀}
(h : b = 0 → a = 0) :
theorem
mul_div_mul_left
{G₀ : Type u_2}
[comm_group_with_zero G₀]
(a b : G₀)
{c : G₀}
(hc : c ≠ 0) :
@[simp]
@[simp]
@[simp]
theorem
semiconj_by.inv_symm_left_iff₀
{G₀ : Type u_2}
[group_with_zero G₀]
{a x y : G₀} :
semiconj_by a⁻¹ x y ↔ semiconj_by a y x
theorem
semiconj_by.inv_symm_left₀
{G₀ : Type u_2}
[group_with_zero G₀]
{a x y : G₀}
(h : semiconj_by a x y) :
semiconj_by a⁻¹ y x
theorem
semiconj_by.inv_right₀
{G₀ : Type u_2}
[group_with_zero G₀]
{a x y : G₀}
(h : semiconj_by a x y) :
semiconj_by a x⁻¹ y⁻¹
@[simp]
theorem
semiconj_by.inv_right_iff₀
{G₀ : Type u_2}
[group_with_zero G₀]
{a x y : G₀} :
semiconj_by a x⁻¹ y⁻¹ ↔ semiconj_by a x y
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]
@[simp]
@[simp]
@[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) :
@[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) :
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 : G₀ →*₀ M₀)
{a : G₀} :
@[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 : G₀ →*₀ M₀)
{a : G₀} :
@[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 : 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 : G₀ →*₀ G₀')
(a b : G₀) :
Inversion on a commutative group with zero, considered as a monoid with zero homomorphism.
Equations
- inv_monoid_with_zero_hom = {to_fun := has_inv.inv (div_inv_monoid.to_has_inv G₀), map_zero' := _, map_one' := _, map_mul' := _}
@[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 : M →*₀ G₀)
(u : 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
- group_with_zero_of_is_unit_or_eq_zero h = {mul := monoid_with_zero.mul hM, mul_assoc := _, one := monoid_with_zero.one hM, one_mul := _, mul_one := _, npow := monoid_with_zero.npow hM, npow_zero' := _, npow_succ' := _, zero := monoid_with_zero.zero hM, zero_mul := _, mul_zero := _, inv := λ (a : M), dite (a = 0) (λ (h0 : a = 0), 0) (λ (h0 : ¬a = 0), ↑(_.unit)⁻¹), div := div_inv_monoid.div._default monoid_with_zero.mul monoid_with_zero.mul_assoc monoid_with_zero.one monoid_with_zero.one_mul monoid_with_zero.mul_one monoid_with_zero.npow monoid_with_zero.npow_zero' monoid_with_zero.npow_succ' (λ (a : M), dite (a = 0) (λ (h0 : a = 0), 0) (λ (h0 : ¬a = 0), ↑(_.unit)⁻¹)), div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default monoid_with_zero.mul monoid_with_zero.mul_assoc monoid_with_zero.one monoid_with_zero.one_mul monoid_with_zero.mul_one monoid_with_zero.npow monoid_with_zero.npow_zero' monoid_with_zero.npow_succ' (λ (a : M), dite (a = 0) (λ (h0 : a = 0), 0) (λ (h0 : ¬a = 0), ↑(_.unit)⁻¹)), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}
noncomputable
def
comm_group_with_zero_of_is_unit_or_eq_zero
{M : Type u_5}
[nontrivial M]
[hM : comm_monoid_with_zero M]
(h : ∀ (a : M), is_unit a ∨ a = 0) :
Constructs a comm_group_with_zero structure on a comm_monoid_with_zero
consisting only of units and 0.
Equations
- comm_group_with_zero_of_is_unit_or_eq_zero h = {mul := group_with_zero.mul (group_with_zero_of_is_unit_or_eq_zero h), mul_assoc := _, one := group_with_zero.one (group_with_zero_of_is_unit_or_eq_zero h), one_mul := _, mul_one := _, npow := group_with_zero.npow (group_with_zero_of_is_unit_or_eq_zero h), npow_zero' := _, npow_succ' := _, mul_comm := _, zero := group_with_zero.zero (group_with_zero_of_is_unit_or_eq_zero h), zero_mul := _, mul_zero := _, inv := group_with_zero.inv (group_with_zero_of_is_unit_or_eq_zero h), div := group_with_zero.div (group_with_zero_of_is_unit_or_eq_zero h), div_eq_mul_inv := _, zpow := group_with_zero.zpow (group_with_zero_of_is_unit_or_eq_zero h), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}