coe — Mathlib

English

The actions satisfy associativity: (s • g) • z = s • (g • z) for s ∈ SL(2, ℤ), g ∈ GL(2, ℝ)⁺, z ∈ ℍ.

Русский

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

LaTeX

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

Lean4

/-- Canonical embedding of `SL(2, ℤ)` into `GL(2, ℝ)⁺`. -/
@[coe]
def coe (g : SL(2, ℤ)) : GL(2, ℝ)⁺ :=
  ((g : SL(2, ℝ)) : GL(2, ℝ)⁺)

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