Mathlib Map

Theorems · Inductive type · group theory

AddCommMagma

Type u → Type u

A commutative additive magma is a type with an addition which commutes.

Defined in
Mathlib.Algebra.Group.Defs
Cited by
32 results in Mathlib
Foundations
Depth 0 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

add_comm · cited by 1535add_commAddCommute.all · cited by 12AddCommute.allle_iff_exists_add' · cited by 7le_iff_exists_add'closedBall_add_singleton · cited by 2closedBall_add_singletonsphere_add_singleton · cited by 2sphere_add_singletonaddLeftEmbedding_eq_addRightEmbedding · cited by 2addLeftEmbedding_eq_addRi…isAddLeftRegular_iff_isAddRegular · cited by 1isAddLeftRegular_iff_isAd…AddSubmonoid.LocalizationMap.injective_iff · cited by 1LocalizationMap.injective…WithBot.le_add_self · cited by 1WithBot.le_add_selfle_map_add_map_div · cited by 1le_map_add_map_divle_map_add_map_sub · cited by 1le_map_add_map_subisAddRightRegular_iff_isAddRegular · cited by 1isAddRightRegular_iff_isA…AddCommMagma.add_comm · cited by 1AddCommMagma.add_commAddCommMagma.ext · cited by 1AddCommMagma.extAddCommMagma.IsLeftCancelAdd.toIsCancelAdd · cited by 1IsLeftCancelAdd.toIsCance…AddCommMagmaCITED BYCITES

Cites0

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Nothing in Mathlib beyond the foundations.

Cited by43

Results whose statement or proof uses this declaration.