norm_σ

Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

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

English

For any g ∈ GL(2,R) and z ∈ ℂ, the complex modulus is preserved under the action: ‖σ(g) z‖ = ‖z‖.

Русский

Для любых g ∈ GL(2, ℝ) и z ∈ ℂ выполняется ‖σ(g) z‖ = ‖z‖; модуль сохраняется.

LaTeX

$$$\\\\|\\\\sigma(g)z\\\\| =\\\\|z\\\\|$$$

Lean4

@[simp]
theorem norm_σ (g : GL (Fin 2) ℝ) (z : ℂ) : ‖σ g z‖ = ‖z‖ :=
  by
  simp only [σ]
  split_ifs <;> simp

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

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

Разделы

Аффилиация

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