Structures · Data types
AddCommMonoidWithOne
An AddCommMonoidWithOne is an AddMonoidWithOne satisfying a + b = b + a.
- Defined in
- Mathlib.Data.Nat.Cast.Defs
- Shape
- One type argument · adds add_comm
Extends2
Extended by2
Concrete types that are instances19
- Nat
- ENNReal
- Filter.Germ
- CStarMatrix
- TensorProduct
- Matrix
- HahnSeries
- QuadraticAlgebra
- EReal
- DirectLimit
- PiTensorProduct
- OrderDual
- ULift
- MulOpposite
- Lex
- AddOpposite
- WithTop
- WithBot
- Submodule
How is a type an instance?
Loading the hierarchy index…
Assumed by61
- Nat.cast_sum
- Finset.sum_boole
- CharZero.of_module
- Matrix.trace_one
- Nat.cast_multiset_sum
- AddConstMapClass.map_nat_add'
- AddConstMapClass.map_nat_add
- Algebra.TensorProduct.one_def
- AddCommGroup.natCast_modEq_natCast
- Nat.cast_finsum_mem
- FirstOrder.Language.presburger.realize_sum
- Algebra.TensorProduct.intCast_def
- SimpleGraph.degree_eq_sum_if_adj
- Algebra.TensorProduct.natCast_def
- Matrix.one_kroneckerTMul_one
- Finset.natCast_card_filter
- WithBot.addCommMonoidWithOne
- ULift.addCommMonoidWithOne
- AddCommMonoidWithOne.add_comm
- SkewMonoidAlgebra.support_one
- PiTensorProduct.instAddCommMonoidWithOne
- QuadraticAlgebra.re_natCast
- Nat.cast_finsupp_sum
- Filter.Germ.instAddCommMonoidWithOne
- Function.Injective.addCommMonoidWithOne
- Algebra.TensorProduct.natCast_def'
- Mathlib.Tactic.Bound.Nat.one_le_cast_of_le
- Function.Surjective.addCommMonoidWithOne
- Algebra.TensorProduct.instOneTensorProduct
- CStarMatrix.instAddCommMonoidWithOne
- PiTensorProduct.instOne
- AddOpposite.instAddCommMonoidWithOne
- QuadraticAlgebra.im_ofNat
- Nat.cast_finsum
- QuadraticAlgebra.C_natCast
- HahnSeries.instAddCommMonoidWithOne
- OrderDual.instAddCommMonoidWithOne
- PiTensorProduct.one_def
- CharZero.of_addMonoidHom
- AddCommMonoidWithOne.toAddCommMonoid
- AddCommMonoidWithOne.toAddMonoidWithOne
- AddConstMapClass.map_ofNat_add'
- WithTop.addCommMonoidWithOne
- AddConstMapClass.map_one_add
- Matrix.trace_permutation
- QuadraticAlgebra.instAddCommMonoidWithOne
- Matrix.sum_single_ofNat
- Algebra.TensorProduct.instAddCommMonoidWithOne
- DirectLimit.instAddCommMonoidWithOneOfAddMonoidHomClass
- Matrix.sum_single_natCast