Theorems · Theorem · number theory

ModularGroup.cases_of_mem_fd_smul_mem_fd

∀ {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} {z : UpperHalfPlane},
  z ∈ ModularGroup.fd →
    g • z ∈ ModularGroup.fd →
      (g = 1 ∨ g = -1) ∨
        (g = ModularGroup.T ∨ g = -ModularGroup.T) ∧ z.re = -1 / 2 ∨
          (g = ModularGroup.T⁻¹ ∨ g = -ModularGroup.T⁻¹) ∧ z.re = 1 / 2 ∨
            (g = ModularGroup.S ∨ g = -ModularGroup.S) ∧ ‖↑z‖ = 1 ∨
              (g = ModularGroup.T * ModularGroup.S ∨ g = -(ModularGroup.T * ModularGroup.S)) ∧
                  z = 1 +ᵥ UpperHalfPlane.ρ ∨
                (g = ModularGroup.T⁻¹ * ModularGroup.S * ModularGroup.T⁻¹ ∨
                      g = -(ModularGroup.T⁻¹ * ModularGroup.S * ModularGroup.T⁻¹)) ∧
                    z = 1 +ᵥ UpperHalfPlane.ρ ∨
                  (g = ModularGroup.S * ModularGroup.T⁻¹ ∨ g = -(ModularGroup.S * ModularGroup.T⁻¹)) ∧
                      z = 1 +ᵥ UpperHalfPlane.ρ ∨
                    (g = ModularGroup.S * ModularGroup.T ∨ g = -(ModularGroup.S * ModularGroup.T)) ∧
                        z = UpperHalfPlane.ρ ∨
                      (g = ModularGroup.T * ModularGroup.S * ModularGroup.T ∨
                            g = -(ModularGroup.T * ModularGroup.S * ModularGroup.T)) ∧
                          z = UpperHalfPlane.ρ ∨
                        (g = ModularGroup.T⁻¹ * ModularGroup.S ∨ g = -(ModularGroup.T⁻¹ * ModularGroup.S)) ∧
                          z = UpperHalfPlane.ρ

Classify the z and g with z ∈ 𝒟 and g • z ∈ 𝒟.

Defined in

Mathlib.NumberTheory.Modular

Cited by

2 results in Mathlib

Foundations

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