Structures · Algebra
GradedMonoid.GMonoid
A graded version of Monoid
Like Monoid.npow, this has an optional GMonoid.gnpow field to allow definitional control of
natural powers of a graded monoid.
- Defined in
- Mathlib.Algebra.GradedMonoid
- Shape
- One type argument · adds one_mul, mul_one, mul_assoc, gnpow, gnpow_zero', gnpow_succ'
Extends2
Extended by2
Concrete types that are instances1
- Nat
How is a type an instance?
Loading the hierarchy index…
Assumed by32
- List.dProd
- GradedMonoid.GMonoid.gnpow
- DirectSum.gsmulHom
- DirectSum.Gmodule.smulAddMonoidHom
- GradedMonoid.mk_list_dProd
- GradedMonoid.GMonoid.gnpow_zero'
- GradedMonoid.GMonoid.gnpow_succ'
- DirectSum.Gmodule.smulAddMonoidHom_apply_of_of
- DirectSum.gsmulHom_apply_apply
- GradedMonoid.list_prod_map_eq_dProd
- GradedMonoid.GradeZero.monoid
- GradedMonoid.fst_pow
- GradedMonoid.GradeZero.mulAction
- GradedMonoid.snd_pow
- List.dProd_nil
- GradedMonoid.GMonoid.mul_one
- GradedMonoid.GMonoid.toGMul
- GradedMonoid.GMonoid.toMonoid
- GradedMonoid.mk_zero_pow
- DirectSum.Gmodule.instSMulOfDecidableEq
- GradedMonoid.GMonoid.toGOne
- GradedMonoid.GMulAction.toMulAction
- List.dProd_cons
- DirectSum.Gmodule.smul_def
- GradedMonoid.instNatPowOfNat
- GradedMonoid.list_prod_ofFn_eq_dProd
- GradedMonoid.GMonoid.toGMulAction
- GradedMonoid.GMonoid.mul_assoc
- DirectSum.Gmodule.of_smul_of
- GradedMonoid.mk_pow
- GradedMonoid.GMonoid.one_mul
- GradedMonoid.mkZeroMonoidHom