instPowNat — Mathlib

English

NumDenSameDeg 𝒜 x forms a commutative monoid with the operations defined as above.

Русский

NumDenSameDeg 𝒜 x образует коммутативный моноид с определёнными операциями.

LaTeX

$$$\\mathrm{NumDenSameDeg}_{\\mathcal{A}}{x} \\text{ is a CommMonoid with } 1,\\; *,$$$

Lean4

instance : Pow (NumDenSameDeg 𝒜 x) ℕ where
  pow c
    n :=
    ⟨n • c.deg, @GradedMonoid.GMonoid.gnpow _ (fun i => ↥(𝒜 i)) _ _ n _ c.num,
      @GradedMonoid.GMonoid.gnpow _ (fun i => ↥(𝒜 i)) _ _ n _ c.den, by
      induction n with
      | zero => simp only [coe_gnpow, pow_zero, one_mem]
      | succ n ih => simpa only [pow_succ, coe_gnpow] using x.mul_mem ih c.den_mem⟩

Похожие утверждения