Structures · Algebra
NatPowAssoc
A mixin for power-associative multiplication.
- Defined in
- Mathlib.Algebra.Group.NatPowAssoc
- Shape
- One type argument · adds npow_add, npow_zero, npow_one
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Complex.UnitClosedDisc
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by55
- npow_one
- npow_zero
- Polynomial.smeval_mul
- Ring.descPochhammer_eq_factorial_smul_choose
- npow_add
- Polynomial.smeval_comp
- Ring.choose_natCast
- Polynomial.ascPochhammer_smeval_cast
- Ring.choose_neg
- npow_mul_assoc
- Ring.multichoose_zero_right
- Polynomial.smeval_mul_X
- Polynomial.descPochhammer_smeval_eq_ascPochhammer
- Ring.multichoose_succ_succ
- Ring.ascPochhammer_succ_succ
- NatPowAssoc.npow_add
- Polynomial.smeval_at_natCast
- Ring.choose_zero_ite
- Polynomial.smeval_X_pow_mul
- Ring.descPochhammer_succ_succ_smeval
- NatPowAssoc.npow_one
- Ring.multichoose_succ_neg_natCast
- Polynomial.smeval_pow
- Int.cast_npow
- Polynomial.smeval_neg_nat
- Ring.choose_zero_succ
- Polynomial.descPochhammer_smeval_eq_descFactorial
- npow_mul
- NatPowAssoc.npow_zero
- Ring.multichoose_zero_succ
- Polynomial.smeval_X_mul
- Ring.choose_smul_choose
- Ring.choose_zero_right
- Ring.choose_add_smul_choose
- Ring.multichoose_one
- Polynomial.smeval_monomial_mul
- Nat.cast_npow
- Ring.choose_zero_pos
- Polynomial.ascPochhammer_smeval_neg_eq_descPochhammer
- Ring.choose_succ_succ
- Polynomial.smeval_at_zero
- Ring.choose_neg'
- Polynomial.smeval_assoc_X_pow
- neg_npow_assoc
- npow_mul_comm
- Ring.multichoose_one_right
- Pi.instNatPowAssoc
- Polynomial.smeval_X_pow_assoc
- Ring.smeval_ascPochhammer_int_ofNat
- Polynomial.smeval_mul_X_pow
Ancestors0
No ancestors.