Typeclasses for groups with an adjoined zero element #
This file provides just the typeclass definitions, and the projection lemmas that expose their members.
Main definitions #
@[instance]
@[class]
Typeclass for expressing that a type M₀ with multiplication and a zero satisfies
0 * a = 0 and a * 0 = 0 for all a : M₀.
Instances
- semigroup_with_zero.to_mul_zero_class
- mul_zero_one_class.to_mul_zero_class
- non_unital_non_assoc_semiring.to_mul_zero_class
- with_zero.mul_zero_class
- prod.mul_zero_class
- order_dual.mul_zero_class
- with_top.mul_zero_class
- with_bot.mul_zero_class
- pi.mul_zero_class
- mul_opposite.mul_zero_class
- add_opposite.mul_zero_class
@[instance]
@[class]
Predicate typeclass for expressing that a * b = 0 implies a = 0 or b = 0
for all a and b of type G₀.
Instances
- cancel_monoid_with_zero.to_no_zero_divisors
- group_with_zero.no_zero_divisors
- is_domain.to_no_zero_divisors
- canonically_ordered_comm_semiring.to_no_zero_divisors
- with_top.no_zero_divisors
- with_bot.no_zero_divisors
- mul_opposite.no_zero_divisors
- add_opposite.no_zero_divisors
- set.set_semiring.no_zero_divisors
- associates.no_zero_divisors
- subsemiring_class.no_zero_divisors
- subsemiring.no_zero_divisors
- subring.no_zero_divisors
- ideal.no_zero_divisors
- subalgebra.no_zero_divisors
- polynomial.no_zero_divisors
- hahn_series.no_zero_divisors
@[instance]
@[instance]
@[class]
- one : M₀
- mul : M₀ → M₀ → M₀
- one_mul : ∀ (a : M₀), 1 * a = a
- mul_one : ∀ (a : M₀), a * 1 = a
- zero : M₀
- zero_mul : ∀ (a : M₀), 0 * a = 0
- mul_zero : ∀ (a : M₀), a * 0 = 0
A typeclass for non-associative monoids with zero elements.
Instances
- monoid_with_zero.to_mul_zero_one_class
- non_assoc_semiring.to_mul_zero_one_class
- with_zero.mul_zero_one_class
- prod.mul_zero_one_class
- order_dual.mul_zero_one_class
- with_top.mul_zero_one_class
- with_bot.mul_zero_one_class
- pi.mul_zero_one_class
- mul_opposite.mul_zero_one_class
- add_opposite.mul_zero_one_class
@[instance]
@[instance]
@[instance]
@[instance]
@[class]
- mul : M₀ → M₀ → M₀
- mul_assoc : ∀ (a b c : M₀), (a * b) * c = a * b * c
- one : M₀
- one_mul : ∀ (a : M₀), 1 * a = a
- mul_one : ∀ (a : M₀), a * 1 = a
- npow : ℕ → M₀ → M₀
- npow_zero' : (∀ (x : M₀), monoid_with_zero.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : M₀), monoid_with_zero.npow n.succ x = x * monoid_with_zero.npow n x) . "try_refl_tac"
- zero : M₀
- zero_mul : ∀ (a : M₀), 0 * a = 0
- mul_zero : ∀ (a : M₀), a * 0 = 0
A type M₀ is a “monoid with zero” if it is a monoid with zero element, and 0 is left
and right absorbing.
Instances
- cancel_monoid_with_zero.to_monoid_with_zero
- comm_monoid_with_zero.to_monoid_with_zero
- group_with_zero.to_monoid_with_zero
- semiring.to_monoid_with_zero
- with_zero.monoid_with_zero
- prod.monoid_with_zero
- order_dual.monoid_with_zero
- with_top.monoid_with_zero
- with_bot.monoid_with_zero
- pi.monoid_with_zero
- mul_opposite.monoid_with_zero
- add_opposite.monoid_with_zero
- real.monoid_with_zero
- nonneg.monoid_with_zero
@[protected, instance]
Equations
- monoid_with_zero.to_semigroup_with_zero M₀ = {mul := monoid_with_zero.mul _inst_1, mul_assoc := _, zero := monoid_with_zero.zero _inst_1, zero_mul := _, mul_zero := _}
@[instance]
def
cancel_monoid_with_zero.to_monoid_with_zero
(M₀ : Type u_4)
[self : cancel_monoid_with_zero M₀] :
@[class]
- mul : M₀ → M₀ → M₀
- mul_assoc : ∀ (a b c : M₀), (a * b) * c = a * b * c
- one : M₀
- one_mul : ∀ (a : M₀), 1 * a = a
- mul_one : ∀ (a : M₀), a * 1 = a
- npow : ℕ → M₀ → M₀
- npow_zero' : (∀ (x : M₀), cancel_monoid_with_zero.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : M₀), cancel_monoid_with_zero.npow n.succ x = x * cancel_monoid_with_zero.npow n x) . "try_refl_tac"
- zero : M₀
- zero_mul : ∀ (a : M₀), 0 * a = 0
- mul_zero : ∀ (a : M₀), a * 0 = 0
- mul_left_cancel_of_ne_zero : ∀ {a b c : M₀}, a ≠ 0 → a * b = a * c → b = c
- mul_right_cancel_of_ne_zero : ∀ {a b c : M₀}, b ≠ 0 → a * b = c * b → a = c
A type M is a cancel_monoid_with_zero if it is a monoid with zero element, 0 is left
and right absorbing, and left/right multiplication by a non-zero element is injective.
theorem
mul_left_cancel₀
{M₀ : Type u_1}
[cancel_monoid_with_zero M₀]
{a b c : M₀}
(ha : a ≠ 0)
(h : a * b = a * c) :
b = c
theorem
mul_right_cancel₀
{M₀ : Type u_1}
[cancel_monoid_with_zero M₀]
{a b c : M₀}
(hb : b ≠ 0)
(h : a * b = c * b) :
a = c
theorem
mul_left_injective₀
{M₀ : Type u_1}
[cancel_monoid_with_zero M₀]
{b : M₀}
(hb : b ≠ 0) :
function.injective (λ (a : M₀), a * b)
@[instance]
def
comm_monoid_with_zero.to_comm_monoid
(M₀ : Type u_4)
[self : comm_monoid_with_zero M₀] :
comm_monoid M₀
@[instance]
@[class]
- mul : M₀ → M₀ → M₀
- mul_assoc : ∀ (a b c : M₀), (a * b) * c = a * b * c
- one : M₀
- one_mul : ∀ (a : M₀), 1 * a = a
- mul_one : ∀ (a : M₀), a * 1 = a
- npow : ℕ → M₀ → M₀
- npow_zero' : (∀ (x : M₀), comm_monoid_with_zero.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : M₀), comm_monoid_with_zero.npow n.succ x = x * comm_monoid_with_zero.npow n x) . "try_refl_tac"
- mul_comm : ∀ (a b : M₀), a * b = b * a
- zero : M₀
- zero_mul : ∀ (a : M₀), 0 * a = 0
- mul_zero : ∀ (a : M₀), a * 0 = 0
A type M is a commutative “monoid with zero” if it is a commutative monoid with zero
element, and 0 is left and right absorbing.
Instances
- cancel_comm_monoid_with_zero.to_comm_monoid_with_zero
- comm_group_with_zero.to_comm_monoid_with_zero
- comm_semiring.to_comm_monoid_with_zero
- linear_ordered_comm_monoid_with_zero.to_comm_monoid_with_zero
- with_zero.comm_monoid_with_zero
- prod.comm_monoid_with_zero
- order_dual.comm_monoid_with_zero
- with_top.comm_monoid_with_zero
- with_bot.comm_monoid_with_zero
- pi.comm_monoid_with_zero
- associates.comm_monoid_with_zero
- real.comm_monoid_with_zero
- nonneg.comm_monoid_with_zero
- nnreal.comm_monoid_with_zero
@[class]
- mul : M₀ → M₀ → M₀
- mul_assoc : ∀ (a b c : M₀), (a * b) * c = a * b * c
- one : M₀
- one_mul : ∀ (a : M₀), 1 * a = a
- mul_one : ∀ (a : M₀), a * 1 = a
- npow : ℕ → M₀ → M₀
- npow_zero' : (∀ (x : M₀), cancel_comm_monoid_with_zero.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : M₀), cancel_comm_monoid_with_zero.npow n.succ x = x * cancel_comm_monoid_with_zero.npow n x) . "try_refl_tac"
- mul_comm : ∀ (a b : M₀), a * b = b * a
- zero : M₀
- zero_mul : ∀ (a : M₀), 0 * a = 0
- mul_zero : ∀ (a : M₀), a * 0 = 0
- mul_left_cancel_of_ne_zero : ∀ {a b c : M₀}, a ≠ 0 → a * b = a * c → b = c
- mul_right_cancel_of_ne_zero : ∀ {a b c : M₀}, b ≠ 0 → a * b = c * b → a = c
A type M is a cancel_comm_monoid_with_zero if it is a commutative monoid with zero element,
0 is left and right absorbing,
and left/right multiplication by a non-zero element is injective.
@[instance]
def
cancel_comm_monoid_with_zero.to_comm_monoid_with_zero
(M₀ : Type u_4)
[self : cancel_comm_monoid_with_zero M₀] :
@[instance]
def
cancel_comm_monoid_with_zero.to_cancel_monoid_with_zero
(M₀ : Type u_4)
[self : cancel_comm_monoid_with_zero M₀] :
@[instance]
@[instance]
@[class]
- mul : G₀ → G₀ → G₀
- mul_assoc : ∀ (a b c : G₀), (a * b) * c = a * b * c
- one : G₀
- one_mul : ∀ (a : G₀), 1 * a = a
- mul_one : ∀ (a : G₀), a * 1 = a
- npow : ℕ → G₀ → G₀
- npow_zero' : (∀ (x : G₀), group_with_zero.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : G₀), group_with_zero.npow n.succ x = x * group_with_zero.npow n x) . "try_refl_tac"
- zero : G₀
- zero_mul : ∀ (a : G₀), 0 * a = 0
- mul_zero : ∀ (a : G₀), a * 0 = 0
- inv : G₀ → G₀
- div : G₀ → G₀ → G₀
- div_eq_mul_inv : (∀ (a b : G₀), a / b = a * b⁻¹) . "try_refl_tac"
- zpow : ℤ → G₀ → G₀
- zpow_zero' : (∀ (a : G₀), group_with_zero.zpow 0 a = 1) . "try_refl_tac"
- zpow_succ' : (∀ (n : ℕ) (a : G₀), group_with_zero.zpow (int.of_nat n.succ) a = a * group_with_zero.zpow (int.of_nat n) a) . "try_refl_tac"
- zpow_neg' : (∀ (n : ℕ) (a : G₀), group_with_zero.zpow -[1+ n] a = (group_with_zero.zpow ↑(n.succ) a)⁻¹) . "try_refl_tac"
- exists_pair_ne : ∃ (x y : G₀), x ≠ y
- inv_zero : 0⁻¹ = 0
- mul_inv_cancel : ∀ (a : G₀), a ≠ 0 → a * a⁻¹ = 1
A type G₀ is a “group with zero” if it is a monoid with zero element (distinct from 1)
such that every nonzero element is invertible.
The type is required to come with an “inverse” function, and the inverse of 0 must be 0.
Examples include division rings and the ordered monoids that are the target of valuations in general valuation theory.
@[instance]
@[simp]
@[class]
- mul : G₀ → G₀ → G₀
- mul_assoc : ∀ (a b c : G₀), (a * b) * c = a * b * c
- one : G₀
- one_mul : ∀ (a : G₀), 1 * a = a
- mul_one : ∀ (a : G₀), a * 1 = a
- npow : ℕ → G₀ → G₀
- npow_zero' : (∀ (x : G₀), comm_group_with_zero.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : G₀), comm_group_with_zero.npow n.succ x = x * comm_group_with_zero.npow n x) . "try_refl_tac"
- mul_comm : ∀ (a b : G₀), a * b = b * a
- zero : G₀
- zero_mul : ∀ (a : G₀), 0 * a = 0
- mul_zero : ∀ (a : G₀), a * 0 = 0
- inv : G₀ → G₀
- div : G₀ → G₀ → G₀
- div_eq_mul_inv : (∀ (a b : G₀), a / b = a * b⁻¹) . "try_refl_tac"
- zpow : ℤ → G₀ → G₀
- zpow_zero' : (∀ (a : G₀), comm_group_with_zero.zpow 0 a = 1) . "try_refl_tac"
- zpow_succ' : (∀ (n : ℕ) (a : G₀), comm_group_with_zero.zpow (int.of_nat n.succ) a = a * comm_group_with_zero.zpow (int.of_nat n) a) . "try_refl_tac"
- zpow_neg' : (∀ (n : ℕ) (a : G₀), comm_group_with_zero.zpow -[1+ n] a = (comm_group_with_zero.zpow ↑(n.succ) a)⁻¹) . "try_refl_tac"
- exists_pair_ne : ∃ (x y : G₀), x ≠ y
- inv_zero : 0⁻¹ = 0
- mul_inv_cancel : ∀ (a : G₀), a ≠ 0 → a * a⁻¹ = 1
A type G₀ is a commutative “group with zero”
if it is a commutative monoid with zero element (distinct from 1)
such that every nonzero element is invertible.
The type is required to come with an “inverse” function, and the inverse of 0 must be 0.
@[instance]
@[instance]
def
comm_group_with_zero.to_comm_monoid_with_zero
(G₀ : Type u_4)
[self : comm_group_with_zero G₀] :