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 #
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
- monoid_with_zero.to_mul_zero_class
- prod.mul_zero_class
- pi.mul_zero_class
- with_zero.mul_zero_class
- with_top.mul_zero_class
- set.set_semiring.mul_zero_class
- monoid_algebra.mul_zero_class
- add_monoid_algebra.mul_zero_class
- direct_sum.mul_zero_class
- ulift.mul_zero_class
- filter.germ.mul_zero_class
- finsupp.mul_zero_class
- locally_constant.mul_zero_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
- domain.to_no_zero_divisors
- canonically_ordered_semiring.canonically_ordered_comm_semiring.to_no_zero_divisors
- with_top.no_zero_divisors
- opposite.no_zero_divisors
- subsemiring.no_zero_divisors
- subring.no_zero_divisors
- subalgebra.no_zero_divisors
- associates.no_zero_divisors
- ideal.no_zero_divisors
- polynomial.no_zero_divisors
- mul : M₀ → M₀ → M₀
- mul_assoc : ∀ (a b c_1 : M₀), (a * b) * c_1 = a * b * c_1
- one : 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 type M
is a “monoid with zero” if it is a monoid with zero element, and 0
is left
and right absorbing.
- mul : M₀ → M₀ → M₀
- mul_assoc : ∀ (a b c_1 : M₀), (a * b) * c_1 = a * b * c_1
- one : 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
- mul_left_cancel_of_ne_zero : ∀ {a b c_1 : M₀}, a ≠ 0 → a * b = a * c_1 → b = c_1
- mul_right_cancel_of_ne_zero : ∀ {a b c_1 : M₀}, b ≠ 0 → a * b = c_1 * b → a = c_1
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.
- mul : M₀ → M₀ → M₀
- mul_assoc : ∀ (a b c_1 : M₀), (a * b) * c_1 = a * b * c_1
- one : M₀
- one_mul : ∀ (a : M₀), 1 * a = a
- mul_one : ∀ (a : M₀), a * 1 = a
- 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
- comm_cancel_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
- prod.comm_monoid_with_zero
- pi.comm_monoid_with_zero
- with_zero.comm_monoid_with_zero
- associates.comm_monoid_with_zero
- mul : M₀ → M₀ → M₀
- mul_assoc : ∀ (a b c_1 : M₀), (a * b) * c_1 = a * b * c_1
- one : M₀
- one_mul : ∀ (a : M₀), 1 * a = a
- mul_one : ∀ (a : M₀), a * 1 = a
- 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_1 : M₀}, a ≠ 0 → a * b = a * c_1 → b = c_1
- mul_right_cancel_of_ne_zero : ∀ {a b c_1 : M₀}, b ≠ 0 → a * b = c_1 * b → a = c_1
A type M
is a comm_cancel_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.
- mul : G₀ → G₀ → G₀
- mul_assoc : ∀ (a b c_1 : G₀), (a * b) * c_1 = a * b * c_1
- one : G₀
- one_mul : ∀ (a : G₀), 1 * a = a
- mul_one : ∀ (a : G₀), a * 1 = 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"
- 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.
- mul : G₀ → G₀ → G₀
- mul_assoc : ∀ (a b c_1 : G₀), (a * b) * c_1 = a * b * c_1
- one : G₀
- one_mul : ∀ (a : G₀), 1 * a = a
- mul_one : ∀ (a : G₀), a * 1 = a
- 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"
- 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
.