Theorems · Theorem · number theory

ModularForm.gnpow_eq_pow

∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetPlusMinusOne] {k : ℤ} (f : ModularForm Γ k) (n : ℕ),
  ⟨n • k, GradedMonoid.GMonoid.gnpow n f⟩ = ⟨↑n * k, f.pow n⟩

Bridge between the auto-derived graded-monoid power GradedMonoid.GMonoid.gnpow and the bespoke ModularForm.pow: as elements of GradedMonoid (ModularForm Γ), the pair ⟨n • k, gnpow n f⟩ agrees with ⟨n * k, f.pow n⟩.

Defined in

Mathlib.NumberTheory.ModularForms.Basic

Cited by

0 results in Mathlib

Foundations

Depth 199 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Subgroup.HasDetPlusMinusOne