Theorems · Theorem · number theory

SlashInvariantForm.slash_action_generators

∀ {f : UpperHalfPlane → ℂ} {Γ : Subgroup (GL (Fin 2) ℝ)} {s : Set (GL (Fin 2) ℝ)},
  Γ = Subgroup.closure s → ∀ {k : ℤ}, (∀ γ ∈ Γ, SlashAction.map k γ f = f) ↔ ∀ γ ∈ s, SlashAction.map k γ f = f

Defined in

Mathlib.NumberTheory.ModularForms.Identities

Cited by

1 results in Mathlib

Foundations

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