T1 in general: matrices of Newman's form (8′) normalize Γ₀(N) ([Nw §1])

With N = e·m·h² (h = h(N), n = N/h² = e·m), g = (ε/√e)·G, G = [[ae, b/h], [Nc/h, de]], and γ = [[x, y], [Nz, x + hf]] ∈ Γ₀(N) (t ≡ x mod h because units mod h ∣ 24 square to 1), G γ adj(G) = e·M with M the explicit integer matrix below (checked in sympy first). Also conjGamma0n_le_normalizer: D⁻¹Γ₀(n)D consists of (8′)-matrices with e = 1.

theorem CongruenceNormalizers.smul_mul_mul_smul_eq_of {s Q : ℝ} (hs : s * s * Q = 1) {W γ A X : Matrix (Fin 2) (Fin 2) ℝ} (h : W * γ * A = Q • X) : s • W * γ * s • A = X

theorem CongruenceNormalizers.hPart_sq_mul_nPart (N : ℕ) (hN : N ≠ 0) : nPart N * hPart N ^ 2 = N

theorem CongruenceNormalizers.isNewmanForm_inv {N : ℕ} {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hg : IsNewmanForm N g) : IsNewmanForm N g⁻¹

theorem CongruenceNormalizers.isNewmanForm_conj_mem {N : ℕ} [NeZero N] {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hg : IsNewmanForm N g) {γ : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hγ : γ ∈ Gamma0R N) : g * γ * g⁻¹ ∈ Gamma0R N

theorem CongruenceNormalizers.newmanForm_mem_normalizer' {N : ℕ} [NeZero N] {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hg : IsNewmanForm N g) : g ∈ Norm0 N

T1 in general.

D⁻¹Γ₀(n)D

theorem CongruenceNormalizers.coe_projSL (A : Matrix (Fin 2) (Fin 2) ℝ) (hA : 0 < A.det) : ↑(projSL A) = (√A.det)⁻¹ • A

theorem CongruenceNormalizers.coe_Dsl (N : ℕ) : ↑(Dsl N) = (√↑(hPart N))⁻¹ • !![↑(hPart N), 0; 0, 1]

theorem CongruenceNormalizers.conjGamma0n_isNewmanForm {N : ℕ} [NeZero N] {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hg : g ∈ conjGamma0n N) : IsNewmanForm N g

theorem CongruenceNormalizers.conjGamma0n_le_normalizer' (N : ℕ) [NeZero N] : conjGamma0n N ≤ Norm0 N