Theorems · Definition · ring theory
GradedMonoid.GMonoid.gnpow
{ι : Type u_1} →
{A : ι → Type u_2} → {inst : AddMonoid ι} → [self : GradedMonoid.GMonoid A] → (n : ℕ) → {i : ι} → A i → A (n • i)Optional field to allow definitional control of natural powers
- Defined in
- Mathlib.Algebra.GradedMonoid
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
- Assumes
- GradedMonoid.GMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddMonoidstatement and proof · cited by 2,864
- GradedMonoid.GMonoidstatement and proof · cited by 24
Cited by10
Results whose statement or proof uses this declaration.
- DirectSum.ofPowstatement and proof · cited by 1
- GradedMonoid.GMonoid.gnpow_succ'statement · cited by 1
- GradedMonoid.GMonoid.gnpow_zero'statement · cited by 1
- ModularForm.qExpansion_of_powproof · cited by 0
- Monoid.gMonoid_gnpowstatement and proof · cited by 0
- ModularForm.gnpow_eq_powstatement and proof · cited by 0
- GradedMonoid.mk_powstatement · cited by 0
- GradedMonoid.mk_zero_powproof · cited by 0
- GradedMonoid.snd_powstatement · cited by 0
- SetLike.coe_gnpowstatement · cited by 0