Theorems · Inductive type · commutative algebra
AddCommMonoidWithOne
Type u_2 → Type u_2
An AddCommMonoidWithOne is an AddMonoidWithOne satisfying a + b = b + a.
- Defined in
- Mathlib.Data.Nat.Cast.Defs
- Cited by
- 42 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
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 by50
Results whose statement or proof uses this declaration.
- Nat.cast_sumstatement and proof · cited by 38
- Finset.sum_boolestatement and proof · cited by 15
- CharZero.of_modulestatement and proof · cited by 4
- NonAssocSemiring.extproof · cited by 4
- Nat.cast_multiset_sumstatement and proof · cited by 2
- AddConstMapClass.map_nat_add'statement and proof · cited by 2
- Matrix.trace_onestatement and proof · cited by 2
- AddCommMonoidWithOne.extstatement and proof · cited by 2
- Matrix.one_kroneckerTMul_onestatement and proof · cited by 1
- AddCommGroup.natCast_modEq_natCaststatement and proof · cited by 1
- Algebra.TensorProduct.intCast_defstatement and proof · cited by 1
- AddConstMapClass.map_nat_addstatement and proof · cited by 1