theorem ModularForm.slash_neg_one {k : ℤ} (f : UpperHalfPlane → ℂ) (hk : Even k) : SlashAction.map ℂ k (-1) f = SlashAction.map ℂ k 1 f

Slash action under -I₂ as a GL(n, ℝ)⁺ matrix. See ModularForm.slash_neg_one' for the SL(2, ℤ) version.

theorem ModularForm.slash_neg_one' {k : ℤ} (f : UpperHalfPlane → ℂ) (hk : Even k) : SlashAction.map ℂ k (-1) f = SlashAction.map ℂ k 1 f

Slash action under -I₂ as a SL(2, ℤ) matrix. See ModularForm.slash_neg_one for the GL(n, ℝ)⁺ version.

theorem ModularForm.slash_neg {k : ℤ} (g : GL (Fin 2) ℝ) (f : UpperHalfPlane → ℂ) (hk : Even k) : SlashAction.map ℂ k (-g) f = SlashAction.map ℂ k g f

See ModularForm.slash_neg' for the version where g is a SL(2, ℤ) matrix.

theorem ModularForm.slash_neg' {k : ℤ} (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (f : UpperHalfPlane → ℂ) (hk : Even k) : SlashAction.map ℂ k (-g) f = SlashAction.map ℂ k g f

See ModularForm.slash_neg for the version where g is a GL(n, ℝ)⁺ matrix.