Typeclasses for (semi)groups and monoid
In this file we define typeclasses for algebraic structures with one binary operation.
The classes are named (add_)?(comm_)?(semigroup|monoid|group)
, where add_
means that
the class uses additive notation and comm_
means that the class assumes that the binary
operation is commutative.
The file does not contain any lemmas except for
- axioms of typeclasses restated in the root namespace;
- lemmas required for instances.
For basic lemmas about these classes see algebra.group.basic
.
A semigroup is a type with an associative (*)
.
Instances
- comm_semigroup.to_semigroup
- left_cancel_semigroup.to_semigroup
- right_cancel_semigroup.to_semigroup
- monoid.to_semigroup
- multiplicative.semigroup
- prod.semigroup
- pi.semigroup
- with_zero.semigroup
- nat.semigroup
- opposite.semigroup
- int.semigroup
- rat.semigroup
- set.semigroup
- matrix.semigroup
- free_abelian_group.semigroup
- magma.free_semigroup.semigroup
- free_semigroup.semigroup
- ulift.semigroup
- continuous_map_semigroup
- real.semigroup
- filter.germ.semigroup
- finsupp.semigroup
- zsqrtd.semigroup
- smooth_map_semigroup
An additive semigroup is a type with an associative (+)
.
Instances
- add_comm_semigroup.to_add_semigroup
- add_left_cancel_semigroup.to_add_semigroup
- add_right_cancel_semigroup.to_add_semigroup
- add_monoid.to_add_semigroup
- additive.add_semigroup
- prod.add_semigroup
- pi.add_semigroup
- with_top.add_semigroup
- with_bot.add_semigroup
- nat.add_semigroup
- opposite.add_semigroup
- int.add_semigroup
- rat.add_semigroup
- set.add_semigroup
- matrix.add_semigroup
- add_magma.free_add_semigroup.add_semigroup
- free_add_semigroup.add_semigroup
- ulift.add_semigroup
- triv_sq_zero_ext.add_semigroup
- continuous_map_add_semigroup
- real.add_semigroup
- filter.germ.add_semigroup
- holor.add_semigroup
- zsqrtd.add_semigroup
- smooth_map_add_semigroup
- game.add_semigroup
- surreal.add_semigroup
- mul : G → G → G
- mul_assoc : ∀ (a b c_1 : G), (a * b) * c_1 = a * b * c_1
- mul_comm : ∀ (a b : G), a * b = b * a
A commutative semigroup is a type with an associative commutative (*)
.
Instances
- comm_monoid.to_comm_semigroup
- comm_ring.to_comm_semigroup
- multiplicative.comm_semigroup
- prod.comm_semigroup
- pi.comm_semigroup
- with_zero.comm_semigroup
- nat.comm_semigroup
- opposite.comm_semigroup
- int.comm_semigroup
- rat.comm_semigroup
- ulift.comm_semigroup
- real.comm_semigroup
- filter.germ.comm_semigroup
- zsqrtd.comm_semigroup
- add : G → G → G
- add_assoc : ∀ (a b c_1 : G), a + b + c_1 = a + (b + c_1)
- add_comm : ∀ (a b : G), a + b = b + a
A commutative additive semigroup is a type with an associative commutative (+)
.
Instances
- add_comm_monoid.to_add_comm_semigroup
- additive.add_comm_semigroup
- prod.add_comm_semigroup
- pi.add_comm_semigroup
- with_top.add_comm_semigroup
- with_bot.add_comm_semigroup
- nat.add_comm_semigroup
- opposite.add_comm_semigroup
- int.add_comm_semigroup
- pnat.add_comm_semigroup
- rat.add_comm_semigroup
- matrix.add_comm_semigroup
- ulift.add_comm_semigroup
- triv_sq_zero_ext.add_comm_semigroup
- real.add_comm_semigroup
- filter.germ.add_comm_semigroup
- pos_num.add_comm_semigroup
- holor.add_comm_semigroup
- zsqrtd.add_comm_semigroup
- game.add_comm_semigroup
- add : G → G → G
- add_assoc : ∀ (a b c_1 : G), a + b + c_1 = a + (b + c_1)
- add_left_cancel : ∀ (a b c_1 : G), a + b = a + c_1 → b = c_1
An add_left_cancel_semigroup
is an additive semigroup such that
a + b = a + c
implies b = c
.
Instances
- add_left_cancel_monoid.to_add_left_cancel_semigroup
- additive.add_left_cancel_semigroup
- prod.left_cancel_add_semigroup
- pi.add_left_cancel_semigroup
- opposite.add_left_cancel_semigroup
- pnat.add_left_cancel_semigroup
- rat.add_left_cancel_semigroup
- finsupp.add_left_cancel_semigroup
- ulift.add_left_cancel_semigroup
- real.add_left_cancel_semigroup
- filter.germ.add_left_cancel_semigroup
- add : G → G → G
- add_assoc : ∀ (a b c_1 : G), a + b + c_1 = a + (b + c_1)
- add_right_cancel : ∀ (a b c_1 : G), a + b = c_1 + b → a = c_1
An add_right_cancel_semigroup
is an additive semigroup such that
a + b = c + b
implies a = c
.
Instances
- add_right_cancel_monoid.to_add_right_cancel_semigroup
- additive.add_right_cancel_semigroup
- prod.right_cancel_add_semigroup
- pi.add_right_cancel_semigroup
- opposite.add_right_cancel_semigroup
- pnat.add_right_cancel_semigroup
- rat.add_right_cancel_semigroup
- finsupp.add_right_cancel_semigroup
- ulift.add_right_cancel_semigroup
- real.add_right_cancel_semigroup
- filter.germ.add_right_cancel_semigroup
- 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
A monoid
is a semigroup
with an element 1
such that 1 * a = a * 1 = a
.
Instances
- comm_monoid.to_monoid
- left_cancel_monoid.to_monoid
- right_cancel_monoid.to_monoid
- div_inv_monoid.to_monoid
- monoid_with_zero.to_monoid
- ring.to_monoid
- monoid.End.monoid
- add_monoid.End.monoid
- multiplicative.monoid
- prod.monoid
- pi.monoid
- ring_hom.monoid
- with_one.monoid
- nat.monoid
- opposite.monoid
- int.monoid
- rat.monoid
- set.monoid
- submonoid.to_monoid
- free_monoid.monoid
- matrix.monoid
- con.monoid
- linear_map.monoid
- Mon.monoid
- category_theory.End.monoid
- Mon.monoid_obj
- Mon.limit_monoid
- category_theory.monoid_discrete
- Mon.colimits.monoid_colimit_type
- ulift.monoid
- ordinal.monoid
- triv_sq_zero_ext.monoid
- filter.monoid
- continuous_monoid
- continuous_map_monoid
- real.monoid
- affine_map.monoid
- filter.germ.monoid
- measure_theory.ae_eq_fun.monoid
- Mon_Type_equivalence_Mon.Mon_monoid
- zsqrtd.monoid
- circle_deg1_lift.monoid
- smooth_map_monoid
- nat.arithmetic_function.monoid
- lucas_lehmer.X.monoid
- add : M → M → M
- add_assoc : ∀ (a b c_1 : M), a + b + c_1 = a + (b + c_1)
- zero : M
- zero_add : ∀ (a : M), 0 + a = a
- add_zero : ∀ (a : M), a + 0 = a
An add_monoid
is an add_semigroup
with an element 0
such that 0 + a = a + 0 = a
.
Instances
- add_comm_monoid.to_add_monoid
- add_left_cancel_monoid.to_add_monoid
- add_right_cancel_monoid.to_add_monoid
- sub_neg_monoid.to_add_monoid
- additive.add_monoid
- prod.add_monoid
- pi.add_monoid
- with_zero.add_monoid
- with_top.add_monoid
- with_bot.add_monoid
- nat.add_monoid
- opposite.add_monoid
- int.add_monoid
- rat.add_monoid
- set.add_monoid
- add_submonoid.to_add_monoid
- free_add_monoid.add_monoid
- matrix.add_monoid
- add_con.add_monoid
- finsupp.add_monoid
- AddMon.add_monoid
- AddMon.add_monoid_obj
- AddMon.limit_add_monoid
- dfinsupp.add_monoid
- ulift.add_monoid
- ordinal.add_monoid
- triv_sq_zero_ext.add_monoid
- filter.add_monoid
- continuous_add_monoid
- continuous_map_add_monoid
- real.add_monoid
- mv_power_series.add_monoid
- power_series.add_monoid
- measure_theory.simple_func.add_monoid
- filter.germ.add_monoid
- measure_theory.ae_eq_fun.add_monoid
- holor.add_monoid
- zsqrtd.add_monoid
- smooth_map_add_monoid
- nat.arithmetic_function.add_monoid
- game.add_monoid
- 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
A commutative monoid is a monoid with commutative (*)
.
Instances
- left_cancel_comm_monoid.to_comm_monoid
- right_cancel_comm_monoid.to_comm_monoid
- comm_group.to_comm_monoid
- comm_monoid_with_zero.to_comm_monoid
- comm_semiring.to_comm_monoid
- ordered_comm_monoid.to_comm_monoid
- linear_ordered_comm_ring.to_comm_monoid
- monoid_hom.comm_monoid
- multiplicative.comm_monoid
- prod.comm_monoid
- pi.comm_monoid
- with_one.comm_monoid
- nat.comm_monoid
- opposite.comm_monoid
- int.comm_monoid
- pnat.comm_monoid
- rat.comm_monoid
- set.comm_monoid
- submonoid.to_comm_monoid
- con.comm_monoid
- associates.comm_monoid
- CommMon.comm_monoid
- CommMon.comm_monoid_obj
- CommMon.limit_comm_monoid
- category_theory.comm_monoid_discrete
- ulift.comm_monoid
- continuous_map_comm_monoid
- localization.comm_monoid
- real.comm_monoid
- filter.germ.comm_monoid
- measure_theory.ae_eq_fun.comm_monoid
- CommMon_Type_equivalence_CommMon.CommMon_comm_monoid
- pos_num.comm_monoid
- zsqrtd.comm_monoid
- perfect_closure.comm_monoid
- smooth_map_comm_monoid
- add : M → M → M
- add_assoc : ∀ (a b c_1 : M), a + b + c_1 = a + (b + c_1)
- zero : M
- zero_add : ∀ (a : M), 0 + a = a
- add_zero : ∀ (a : M), a + 0 = a
- add_comm : ∀ (a b : M), a + b = b + a
An additive commutative monoid is an additive monoid with commutative (+)
.
Instances
- add_left_cancel_comm_monoid.to_add_comm_monoid
- add_right_cancel_comm_monoid.to_add_comm_monoid
- semiring.to_add_comm_monoid
- ordered_add_comm_monoid.to_add_comm_monoid
- add_comm_group.to_add_comm_monoid
- add_monoid_hom.add_comm_monoid
- additive.add_comm_monoid
- prod.add_comm_monoid
- pi.add_comm_monoid
- with_zero.add_comm_monoid
- with_top.add_comm_monoid
- with_bot.add_comm_monoid
- nat.add_comm_monoid
- opposite.add_comm_monoid
- int.add_comm_monoid
- rat.add_comm_monoid
- set.add_comm_monoid
- add_submonoid.to_add_comm_monoid
- matrix.add_comm_monoid
- add_con.add_comm_monoid
- submodule.add_comm_monoid
- enat.add_comm_monoid
- finsupp.add_comm_monoid
- linear_map.add_comm_monoid
- submodule.add_comm_monoid_submodule
- tensor_product.add_comm_monoid
- restrict_scalars.add_comm_monoid
- monoid_algebra.add_comm_monoid
- add_monoid_algebra.add_comm_monoid
- AddCommMon.add_comm_monoid
- AddCommMon.add_comm_monoid_obj
- AddCommMon.limit_add_comm_monoid
- dfinsupp.add_comm_monoid
- direct_sum.add_comm_monoid
- ulift.add_comm_monoid
- multilinear_map.add_comm_monoid
- alternating_map.add_comm_monoid
- bilin_form.add_comm_monoid
- lie_submodule.add_comm_monoid
- triv_sq_zero_ext.add_comm_monoid
- continuous_linear_map.add_comm_monoid
- continuous_map_add_comm_monoid
- add_localization.add_comm_monoid
- real.add_comm_monoid
- continuous_multilinear_map.add_comm_monoid
- mv_power_series.add_comm_monoid
- power_series.add_comm_monoid
- measure_theory.outer_measure.add_comm_monoid
- measure_theory.measure.add_comm_monoid
- measure_theory.simple_func.add_comm_monoid
- filter.germ.add_comm_monoid
- measure_theory.ae_eq_fun.add_comm_monoid
- holor.add_comm_monoid
- zsqrtd.add_comm_monoid
- smooth_map_add_comm_monoid
- pi_tensor_product.add_comm_monoid
- nat.arithmetic_function.add_comm_monoid
- derivation.add_comm_monoid
- add : M → M → M
- add_assoc : ∀ (a b c_1 : M), a + b + c_1 = a + (b + c_1)
- add_left_cancel : ∀ (a b c_1 : M), a + b = a + c_1 → b = c_1
- zero : M
- zero_add : ∀ (a : M), 0 + a = a
- add_zero : ∀ (a : M), a + 0 = a
An additive monoid in which addition is left-cancellative.
Main examples are ℕ
and groups. This is the right typeclass for many sum lemmas, as having a zero
is useful to define the sum over the empty set, so add_left_cancel_semigroup
is not enough.
- add : M → M → M
- add_assoc : ∀ (a b c_1 : M), a + b + c_1 = a + (b + c_1)
- add_left_cancel : ∀ (a b c_1 : M), a + b = a + c_1 → b = c_1
- zero : M
- zero_add : ∀ (a : M), 0 + a = a
- add_zero : ∀ (a : M), a + 0 = a
- add_comm : ∀ (a b : M), a + b = b + a
Commutative version of add_left_cancel_monoid.
- add : M → M → M
- add_assoc : ∀ (a b c_1 : M), a + b + c_1 = a + (b + c_1)
- add_right_cancel : ∀ (a b c_1 : M), a + b = c_1 + b → a = c_1
- zero : M
- zero_add : ∀ (a : M), 0 + a = a
- add_zero : ∀ (a : M), a + 0 = a
An additive monoid in which addition is right-cancellative.
Main examples are ℕ
and groups. This is the right typeclass for many sum lemmas, as having a zero
is useful to define the sum over the empty set, so add_right_cancel_semigroup
is not enough.
- add : M → M → M
- add_assoc : ∀ (a b c_1 : M), a + b + c_1 = a + (b + c_1)
- add_right_cancel : ∀ (a b c_1 : M), a + b = c_1 + b → a = c_1
- zero : M
- zero_add : ∀ (a : M), 0 + a = a
- add_zero : ∀ (a : M), a + 0 = a
- add_comm : ∀ (a b : M), a + b = b + a
Commutative version of add_right_cancel_monoid.
- add : M → M → M
- add_assoc : ∀ (a b c_1 : M), a + b + c_1 = a + (b + c_1)
- add_left_cancel : ∀ (a b c_1 : M), a + b = a + c_1 → b = c_1
- zero : M
- zero_add : ∀ (a : M), 0 + a = a
- add_zero : ∀ (a : M), a + 0 = a
- add_right_cancel : ∀ (a b c_1 : M), a + b = c_1 + b → a = c_1
An additive monoid in which addition is cancellative on both sides.
Main examples are ℕ
and groups. This is the right typeclass for many sum lemmas, as having a zero
is useful to define the sum over the empty set, so add_right_cancel_semigroup
is not enough.
Instances
- mul : M → M → M
- mul_assoc : ∀ (a b c_1 : M), (a * b) * c_1 = a * b * c_1
- mul_left_cancel : ∀ (a b c_1 : M), a * b = a * c_1 → b = c_1
- one : M
- one_mul : ∀ (a : M), 1 * a = a
- mul_one : ∀ (a : M), a * 1 = a
- mul_right_cancel : ∀ (a b c_1 : M), a * b = c_1 * b → a = c_1
A monoid in which multiplication is cancellative.
Instances
- add : M → M → M
- add_assoc : ∀ (a b c_1 : M), a + b + c_1 = a + (b + c_1)
- add_left_cancel : ∀ (a b c_1 : M), a + b = a + c_1 → b = c_1
- zero : M
- zero_add : ∀ (a : M), 0 + a = a
- add_zero : ∀ (a : M), a + 0 = a
- add_comm : ∀ (a b : M), a + b = b + a
- add_right_cancel : ∀ (a b c_1 : M), a + b = c_1 + b → a = c_1
Commutative version of add_cancel_monoid.
- mul : M → M → M
- mul_assoc : ∀ (a b c_1 : M), (a * b) * c_1 = a * b * c_1
- mul_left_cancel : ∀ (a b c_1 : M), a * b = a * c_1 → 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
- mul_right_cancel : ∀ (a b c_1 : M), a * b = c_1 * b → a = c_1
Commutative version of cancel_monoid.
try_refl_tac
solves goals of the form ∀ a b, f a b = g a b
,
if they hold by definition.
- 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
- inv : G → G
- div : G → G → G
- div_eq_mul_inv : (∀ (a b : G), a / b = a * b⁻¹) . "try_refl_tac"
A div_inv_monoid
is a monoid
with operations /
and ⁻¹
satisfying
div_eq_mul_inv : ∀ a b, a / b = a * b⁻¹
.
This is the immediate common ancestor of group
and group_with_zero
,
in order to deduplicate the name div_eq_mul_inv
.
The default for div
is such that a / b = a * b⁻¹
holds by definition.
Adding div
as a field rather than defining a / b := a * b⁻¹
allows us to
avoid certain classes of unification failures, for example:
Let foo X
be a type with a ∀ X, has_div (foo X)
instance but no
∀ X, has_inv (foo X)
, e.g. when foo X
is a euclidean_domain
. Suppose we
also have an instance ∀ X [cromulent X], group_with_zero (foo X)
. Then the
(/)
coming from group_with_zero_has_div
cannot be definitionally equal to
the (/)
coming from foo.has_div
.
- add : G → G → G
- add_assoc : ∀ (a b c_1 : G), a + b + c_1 = a + (b + c_1)
- zero : G
- zero_add : ∀ (a : G), 0 + a = a
- add_zero : ∀ (a : G), a + 0 = a
- neg : G → G
- sub : G → G → G
- sub_eq_add_neg : (∀ (a b : G), a - b = a + -b) . "try_refl_tac"
A sub_neg_monoid
is an add_monoid
with unary -
and binary -
operations
satisfying sub_eq_add_neg : ∀ a b, a - b = a + -b
.
The default for sub
is such that a - b = a + -b
holds by definition.
Adding sub
as a field rather than defining a - b := a + -b
allows us to
avoid certain classes of unification failures, for example:
Let foo X
be a type with a ∀ X, has_sub (foo X)
instance but no
∀ X, has_neg (foo X)
. Suppose we also have an instance
∀ X [cromulent X], add_group (foo X)
. Then the (-)
coming from
add_group.has_sub
cannot be definitionally equal to the (-)
coming from
foo.has_sub
.
- 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
- inv : G → G
- div : G → G → G
- div_eq_mul_inv : (∀ (a b : G), a / b = a * b⁻¹) . "try_refl_tac"
- mul_left_inv : ∀ (a : G), a⁻¹ * a = 1
A group
is a monoid
with an operation ⁻¹
satisfying a⁻¹ * a = 1
.
There is also a division operation /
such that a / b = a * b⁻¹
,
with a default so that a / b = a * b⁻¹
holds by definition.
Instances
- comm_group.to_group
- units.group
- multiplicative.group
- prod.group
- pi.group
- opposite.group
- rel_iso.group
- equiv.perm.perm_group
- subgroup.to_group
- mul_aut.group
- add_aut.group
- ring_aut.group
- con.group
- linear_map.automorphism_group
- alg_equiv.aut
- category_theory.End.group
- category_theory.Aut.group
- Group.group
- Group.group_obj
- Group.limit_group
- free_group.group
- quotient_group.quotient.group
- ulift.group
- rack.envel_group.group
- continuous_linear_equiv.automorphism_group
- continuous_group
- continuous_map_group
- isometric.group
- affine_equiv.group
- filter.germ.group
- measure_theory.ae_eq_fun.group
- smooth_map_group
- dihedral.group
- presented_group.group
- semidirect_product.group
- matrix.special_linear_group.group
- add : A → A → A
- add_assoc : ∀ (a b c_1 : A), a + b + c_1 = a + (b + c_1)
- zero : A
- zero_add : ∀ (a : A), 0 + a = a
- add_zero : ∀ (a : A), a + 0 = a
- neg : A → A
- sub : A → A → A
- sub_eq_add_neg : (∀ (a b : A), a - b = a + -b) . "try_refl_tac"
- add_left_neg : ∀ (a : A), -a + a = 0
An add_group
is an add_monoid
with a unary -
satisfying -a + a = 0
.
There is also a binary operation -
such that a - b = a + -b
,
with a default so that a - b = a + -b
holds by definition.
Instances
- add_comm_group.to_add_group
- add_units.add_group
- additive.add_group
- prod.add_group
- pi.add_group
- opposite.add_group
- rat.add_group
- add_subgroup.to_add_group
- matrix.add_group
- add_con.add_group
- finsupp.add_group
- monoid_algebra.add_group
- add_monoid_algebra.add_group
- AddGroup.add_group
- AddGroup.add_group_obj
- AddGroup.limit_add_group
- dfinsupp.add_group
- quotient_add_group.add_group
- ulift.add_group
- triv_sq_zero_ext.add_group
- continuous_add_group
- continuous_map_add_group
- real.add_group
- mv_power_series.add_group
- power_series.add_group
- measure_theory.simple_func.add_group
- filter.germ.add_group
- measure_theory.ae_eq_fun.add_group
- holor.add_group
- smooth_map_add_group
- nat.arithmetic_function.add_group
- game.add_group
- uniform_space.completion.add_group
Abbreviation for @div_inv_monoid.to_monoid _ (@group.to_div_inv_monoid _ _)
.
Useful because it corresponds to the fact that Grp
is a subcategory of Mon
.
Not an instance since it duplicates @div_inv_monoid.to_monoid _ (@group.to_div_inv_monoid _ _)
.
Equations
Equations
- group.to_cancel_monoid = {mul := group.mul _inst_1, mul_assoc := _, mul_left_cancel := _, one := group.one _inst_1, one_mul := _, mul_one := _, mul_right_cancel := _}
- 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
- inv : G → G
- div : G → G → G
- div_eq_mul_inv : (∀ (a b : G), a / b = a * b⁻¹) . "try_refl_tac"
- mul_left_inv : ∀ (a : G), a⁻¹ * a = 1
- mul_comm : ∀ (a b : G), a * b = b * a
A commutative group is a group with commutative (*)
.
Instances
- ordered_comm_group.to_comm_group
- linear_ordered_comm_group.to_comm_group
- units.comm_group
- monoid_hom.comm_group
- multiplicative.comm_group
- prod.comm_group
- pi.comm_group
- opposite.comm_group
- subgroup.to_comm_group
- punit.comm_group
- CommGroup.comm_group_instance
- CommGroup.comm_group_obj
- CommGroup.limit_comm_group
- quotient_group.quotient.comm_group
- abelianization.comm_group
- ulift.comm_group
- continuous_comm_group
- continuous_map_comm_group
- filter.germ.comm_group
- measure_theory.ae_eq_fun.comm_group
- smooth_map_comm_group
- add : G → G → G
- add_assoc : ∀ (a b c_1 : G), a + b + c_1 = a + (b + c_1)
- zero : G
- zero_add : ∀ (a : G), 0 + a = a
- add_zero : ∀ (a : G), a + 0 = a
- neg : G → G
- sub : G → G → G
- sub_eq_add_neg : (∀ (a b : G), a - b = a + -b) . "try_refl_tac"
- add_left_neg : ∀ (a : G), -a + a = 0
- add_comm : ∀ (a b : G), a + b = b + a
An additive commutative group is an additive group with commutative (+)
.
Instances
- ring.to_add_comm_group
- ordered_add_comm_group.to_add_comm_group
- linear_ordered_add_comm_group.to_add_comm_group
- nonneg_add_comm_group.to_add_comm_group
- lie_ring.to_add_comm_group
- add_group_with_zero_nhd.to_add_comm_group
- normed_group.to_add_comm_group
- add_units.add_comm_group
- add_monoid_hom.add_comm_group
- additive.add_comm_group
- prod.add_comm_group
- pi.add_comm_group
- opposite.add_comm_group
- rat.add_comm_group
- add_subgroup.to_add_comm_group
- matrix.add_comm_group
- submodule.add_comm_group
- finsupp.add_comm_group
- linear_map.add_comm_group
- submodule.quotient.add_comm_group
- tensor_product.add_comm_group
- restrict_scalars.add_comm_group
- punit.add_comm_group
- AddCommGroup.add_comm_group_instance
- Module.is_add_comm_group
- AddCommGroup.add_comm_group_obj
- AddCommGroup.limit_add_comm_group
- dfinsupp.add_comm_group
- direct_sum.add_comm_group
- quotient_add_group.add_comm_group
- free_abelian_group.add_comm_group
- module.direct_limit.add_comm_group
- add_comm_group.direct_limit.add_comm_group
- Module.add_comm_group_obj
- Module.limit_add_comm_group
- AddCommGroup.colimits.colimit_type.add_comm_group
- ulift.add_comm_group
- multilinear_map.add_comm_group
- alternating_map.add_comm_group
- module.dual.add_comm_group
- bilin_form.add_comm_group
- triv_sq_zero_ext.add_comm_group
- continuous_linear_map.add_comm_group
- continuous_add_comm_group
- continuous_map_add_comm_group
- real.add_comm_group
- affine_map.add_comm_group
- bounded_continuous_function.add_comm_group
- continuous_multilinear_map.add_comm_group
- mv_power_series.add_comm_group
- power_series.add_comm_group
- formal_multilinear_series.add_comm_group
- real.angle.angle.add_comm_group
- measure_theory.simple_func.add_comm_group
- filter.germ.add_comm_group
- measure_theory.ae_eq_fun.add_comm_group
- measure_theory.l1.add_comm_group
- sesq_form.add_comm_group
- znum.add_comm_group
- holor.add_comm_group
- padic.add_comm_group
- mv_polynomial.R.add_comm_group
- tangent_space.add_comm_group
- smooth_map_add_comm_group
- quadratic_form.add_comm_group
- pi_tensor_product.add_comm_group
- nat.arithmetic_function.add_comm_group
- lucas_lehmer.X.add_comm_group
- derivation.add_comm_group
- game.add_comm_group
- uniform_space.completion.add_comm_group
Equations
- comm_group.to_cancel_comm_monoid = {mul := comm_group.mul _inst_1, mul_assoc := _, mul_left_cancel := _, one := comm_group.one _inst_1, one_mul := _, mul_one := _, mul_comm := _, mul_right_cancel := _}