English
Let cd: Fin 2 → ℝ, z ∈ ℂ with z.im ≠ 0, and cd ≠ 0. Then (cd0) z + cd1 ≠ 0.
Русский
Пусть cd: Fin 2 → ℝ, z ∈ ℂ с z.im ≠ 0, и cd ≠ 0. Тогда (cd0) z + cd1 ≠ 0.
LaTeX
$$$$ (cd_0) z + cd_1 \\neq 0. $$$$
Lean4
/-- `SL(2, ℝ)` acts on the upper half plane as an isometry. -/
instance : IsIsometricSMul SL(2, ℝ) ℍ :=
⟨fun g =>
by
have h₀ : Isometry (fun z => ModularGroup.S • z : ℍ → ℍ) :=
Isometry.of_dist_eq fun y₁ y₂ =>
by
have h₁ : 0 ≤ im y₁ * im y₂ := mul_nonneg y₁.property.le y₂.property.le
have h₂ : ‖(y₁ * y₂ : ℂ)‖ ≠ 0 := by simp [y₁.ne_zero, y₂.ne_zero]
simp_rw [modular_S_smul, inv_neg, dist_eq, coe_mk, dist_neg_neg, dist_inv_inv₀ y₁.ne_zero y₂.ne_zero, mk_im,
neg_im, inv_im, coe_im, neg_div, neg_neg, div_mul_div_comm, ← normSq_mul, Real.sqrt_div h₁, ← norm_def,
mul_div (2 : ℝ)]
rw [div_div_div_comm, ← norm_mul, div_self h₂, div_one]
by_cases hc : g 1 0 = 0
· obtain ⟨u, v, h⟩ := exists_SL2_smul_eq_of_apply_zero_one_eq_zero g hc
rw [h]
exact (isometry_real_vadd v).comp (isometry_pos_mul u)
· obtain ⟨u, v, w, h⟩ := exists_SL2_smul_eq_of_apply_zero_one_ne_zero g hc
rw [h]
exact (isometry_real_vadd w).comp (h₀.comp <| (isometry_real_vadd v).comp <| isometry_pos_mul u)⟩
