English
There exists a noncomputable instance defining a MulAction of SL(2,R) on the upper half-plane, compatible with the GL action via a restriction to SL(2,R).
Русский
Существет несчислимый экземпляр задающий MulAction SL(2,R) на верхней полуплоскости, совместимый с действием GL через ограничение на SL(2,R).
LaTeX
$$$\\text{MulAction SL(2,R) } \\mathbb{H}$$$
Lean4
theorem specialLinearGroup_apply {R : Type*} [CommRing R] [Algebra R ℝ] (g : SL(2, R)) (z : ℍ) :
g • z =
mk
(((algebraMap R ℝ (g 0 0) : ℂ) * z + (algebraMap R ℝ (g 0 1) : ℂ)) /
((algebraMap R ℝ (g 1 0) : ℂ) * z + (algebraMap R ℝ (g 1 1) : ℂ)))
(coe_specialLinearGroup_apply g z ▸ (g • z).property) :=
by ext;
simp [coe_specialLinearGroup_apply]
/- these next few lemmas are *not* flagged `@simp` because of the constructors on the RHS;
instead we use the versions with coercions to `ℂ` as simp lemmas instead. -/
