σ_ofReal

Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

URI: https://scilib.ai/kg/mathlib#UpperHalfPlane.σ_ofReal

English

For any g ∈ GL(2,ℝ) and y ∈ ℝ, σ g y = y.

Русский

Для любого g ∈ GL(2,ℝ) и y ∈ ℝ, σ g y = y.

LaTeX

$$$$ \\sigma(g)(y) = y \\quad \\text{for } y \\in \\mathbb{R}. $$$$

Lean4

@[simp]
theorem σ_ofReal (g : GL (Fin 2) ℝ) (y : ℝ) : σ g y = y :=
  by
  simp only [σ]
  split_ifs <;> simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru