Structures · Data types
AddCommGroupWithOne
An AddCommGroupWithOne is an AddGroupWithOne satisfying a + b = b + a.
- Defined in
- Mathlib.Data.Int.Cast.Defs
- Shape
- One type argument · adds natCast_zero, natCast_succ, intCast_ofNat, intCast_negSucc
Extends3
Extended by2
Forgetful instances
Provided automatically by
Concrete types that are instances13
- CStarMatrix
- TensorProduct
- Matrix
- HahnSeries
- QuadraticAlgebra
- DirectLimit
- QuaternionAlgebra
- GradedTensorProduct
- OrderDual
- ULift
- MulOpposite
- Lex
- AddOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by80
- Ring.choose
- Int.cast_le
- Int.cast_pos
- Int.cast_lt
- Int.cast_nonneg
- Int.cast_sum
- CategoryTheory.DifferentialObject.shiftFunctor
- Int.cast_mono
- AddCommGroupWithOne.toNatCast
- Int.cast_nonneg_iff
- AddCommGroupWithOne.toIntCast
- AddCommGroup.intCast_modEq_intCast
- AddCommGroupWithOne.toOne
- CategoryTheory.DifferentialObject.shiftFunctorAdd
- CategoryTheory.DifferentialObject.shiftZero
- AddConstMapClass.map_int_add'
- Int.cast_strictMono
- Int.cast_lt_zero
- Algebra.TensorProduct.intCast_def
- ZNum.cast_sub
- AddCommGroupWithOne.natCast_zero
- Int.cast_nonpos
- AddCommGroupWithOne.natCast_succ
- Order.IsPredPrelimit.lt_sub_natCast
- AddCommGroupWithOne.toAddGroupWithOne
- AddCommGroupWithOne.toAddCommGroup
- CategoryTheory.DifferentialObject.shiftFunctor_map_f
- QuaternionAlgebra.instAddCommGroupWithOne
- CategoryTheory.DifferentialObject.shiftFunctorAdd_hom_app_f
- Order.pred_iterate
- HahnSeries.instAddCommGroupWithOne
- QuaternionAlgebra.imJ_natCast
- QuadraticAlgebra.C_intCast
- Order.IsPredLimit.lt_sub_natCast
- QuaternionAlgebra.coe_natCast
- QuaternionAlgebra.im_ofNat
- Matrix.sum_single_intCast
- Int.cast_finsupp_sum
- QuaternionAlgebra.re_ofNat
- CategoryTheory.DifferentialObject.instHasShift
- QuaternionAlgebra.coe_intCast
- QuaternionAlgebra.re_intCast
- AddConstMapClass.map_int_add
- QuadraticAlgebra.re_intCast
- OrderDual.instAddCommGroupWithOne
- AddCommGroup.ModEq.of_intCast
- CategoryTheory.DifferentialObject.shiftZero_hom_app_f
- AddCommGroupWithOne.toAddCommMonoidWithOne
- AddCommGroup.intCast_modEq_intCast'
- QuaternionAlgebra.imI_intCast
Ancestors49
- Add
- AddAction
- AddCancelCommMonoid
- AddCancelMonoid
- AddCommGroup
- AddCommMagma
- AddCommMonoid
- AddCommMonoidWithOne
- AddCommSemigroup
- AddGroup
- AddGroupWithOne
- AddLeftCancelMonoid
- AddLeftCancelSemigroup
- AddMonoid
- AddMonoidWithOne
- AddRightCancelMonoid
- AddRightCancelSemigroup
- AddSemigroup
- AddSemigroupAction
- AddTorsor
- AddZero
- AddZeroClass
- HAdd
- HSub
- HVAdd
- IntCast
- InvolutiveNeg
- IsLeftCancelAdd
- IsRightCancelAdd
- Lean.Grind.AddCommGroup
- Lean.Grind.AddCommMonoid
- Lean.Grind.IntModule
- Lean.Grind.NatModule
- NSMul
- NatCast
- Neg
- NegZeroClass
- Nonempty
- OfNat
- One
- Sub
- SubNegMonoid
- SubNegZeroMonoid
- SubtractionCommMonoid
- SubtractionMonoid
- VAdd
- VSub
- ZSMul
- Zero