SL_to_GL_tower — Mathlib

English

For all s ∈ SL(2, ℤ), g ∈ GL(2, ℝ)⁺, z ∈ ℍ, the scalar actions satisfy (s • g) • z = s • (g • z).

Русский

Для всех s ∈ SL(2, ℤ), g ∈ GL(2, ℝ)⁺, z ∈ ℍ, скалярные действия удовлетворяют (s • g) • z = s • (g • z).

LaTeX

$$$(s \cdot g) \cdot z = s \cdot (g \cdot z)$$

Lean4

instance SL_to_GL_tower : IsScalarTower SL(2, ℤ) GL(2, ℝ)⁺ ℍ where
  smul_assoc s g
    z := by
    simp only [SLOnGLPos_smul_apply]
    apply mul_smul'

Похожие утверждения