Theorems · Theorem · number theory

ModularGroup.lcRow0Extend_symm_apply

∀ {cd : Fin 2 → ℤ} (hcd : IsCoprime (cd 0) (cd 1)) (f : (i : Fin 2) → (fun a => Fin 2 → ℝ) i) (i a : Fin 2),
  (ModularGroup.lcRow0Extend hcd).symm f i a =
    (![(LinearMap.GeneralLinearGroup.generalLinearEquiv ℝ (Fin 2 → ℝ))
              (Matrix.GeneralLinearGroup.toLin (Matrix.planeConformalMatrix (↑(cd 0)) (-↑(cd 1)) ⋯)),
            LinearEquiv.refl ℝ (Fin 2 → ℝ)]
          i).symm
      (f i) a

Defined in

Mathlib.NumberTheory.Modular

Cited by

0 results in Mathlib

Foundations

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