Structures · Algebra
GradedMonoid.GMul
A graded version of Mul. Multiplication combines grades additively, like
AddMonoidAlgebra.
- Defined in
- Mathlib.Algebra.GradedMonoid
- Shape
- One type argument · adds mul
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Concrete types that are instances2
- Int
- Nat
How is a type an instance?
Loading the hierarchy index…
Assumed by13
- GradedMonoid.GMul.mul
- GradedMonoid.GMonoid.gnpowRec
- GradedMonoid.mk_zero_smul
- GradedMonoid.mk_mul_mk
- GradedMonoid.GMul.toMul
- GradedMonoid.GradeZero.smul
- GradedMonoid.snd_mul
- GradedMonoid.GMul.toGSMul
- GradedMonoid.GMonoid.gnpowRec_succ
- GradedMonoid.GradeZero.mul
- GradedMonoid.GradeZero.smul_eq_mul
- GradedMonoid.GMonoid.gnpowRec_zero
- GradedMonoid.fst_mul
Ancestors0
No ancestors.