Theorems · Theorem · number theory

SlashInvariantForm.prod.congr_simp

∀ {ι : Type} {s s_1 : Finset ι} (e_s : s = s_1) {k : ι → ℤ} (m : ℤ) (hm : m = ∑ i ∈ s, k i)
  {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetPlusMinusOne] (f f_1 : (i : ι) → SlashInvariantForm Γ (k i)),
  f = f_1 → SlashInvariantForm.prod m hm f = SlashInvariantForm.prod m ⋯ f_1

Defined in: Mathlib.NumberTheory.ModularForms.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 184 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Subgroup.HasDetPlusMinusOne

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
Finsetstatement and proof · cited by 13,712
Finset.sumstatement and proof · cited by 5,195
Matrixstatement · cited by 4,303
Subgroupstatement and proof · cited by 3,593
Matrix.GeneralLinearGroupstatement and proof · cited by 556
Subgroup.HasDetPlusMinusOnestatement and proof · cited by 57
SlashInvariantFormstatement and proof · cited by 46
SlashInvariantForm.prodstatement and proof · cited by 2

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.