English
An explicit formula expresses g•z in terms of lcRow0 and the bottom row (c,d):\n g•z = (lcRow0(p) g)/(c^2+d^2) + ((d z − c))/((c^2+d^2)(c z + d)).
Русский
Является явное тождество, выражающее g•z через lcRow0(p) и нижнюю строку p=(c,d):\n g•z = (lcRow0(p) g)/(c^2+d^2) + ((d z − c))/((c^2+d^2)(c z + d)).
LaTeX
$$$ g\\cdot z = \\frac{\\operatorname{lcRow0}(p)\\, g}{c^2+d^2} + \\frac{d z - c}{(c^2+d^2)(c z + d)}, \\text{ where } p=(c,d) \\text{ and } \\gcd(c,d)=1.$$$
Lean4
/-- This replaces `(g•z).re = a/c + *` in the standard theory with the following novel identity:
`g • z = (a c + b d) / (c^2 + d^2) + (d z - c) / ((c^2 + d^2) (c z + d))`
which does not need to be decomposed depending on whether `c = 0`. -/
theorem smul_eq_lcRow0_add {p : Fin 2 → ℤ} (hp : IsCoprime (p 0) (p 1)) (hg : g 1 = p) :
↑(g • z) =
(lcRow0 p ↑(g : SL(2, ℝ)) : ℂ) / ((p 0 : ℂ) ^ 2 + (p 1 : ℂ) ^ 2) +
((p 1 : ℂ) * z - p 0) / (((p 0 : ℂ) ^ 2 + (p 1 : ℂ) ^ 2) * (p 0 * z + p 1)) :=
by
have nonZ1 : (p 0 : ℂ) ^ 2 + (p 1 : ℂ) ^ 2 ≠ 0 := mod_cast hp.sq_add_sq_ne_zero
have : ((↑) : ℤ → ℝ) ∘ p ≠ 0 := fun h => hp.ne_zero (by ext i; simpa using congr_fun h i)
have nonZ2 : (p 0 : ℂ) * z + p 1 ≠ 0 := by simpa using linear_ne_zero z this
subst hg
rw [coe_specialLinearGroup_apply]
replace nonZ2 : z * (g 1 0 : ℂ) + g 1 1 ≠ 0 := by convert nonZ2 using 1; ring
have H := congr(Int.cast (R := ℂ) $(det_fin_two g))
simp at H
simp [field]
linear_combination -((z : ℂ) * (g 1 1 : ℂ) - g 1 0) * H
