σ_neg — Mathlib

English

For any invertible 2×2 real matrix g, the Möbius action σ is unchanged when g is replaced by −g; i.e., σ(−g) equals σ(g).

Русский

Пусть g — обратимая матрица размером 2×2 над ℝ. Действие Моебиуса σ не меняется при замене g на −g; то есть σ(−g) = σ(g).

LaTeX

$$$\\\\sigma(-g) = \\\\sigma(g)$$$

Lean4

@[simp]
theorem σ_neg (g : GL (Fin 2) ℝ) : σ (-g) = σ g := by simp [σ, det_neg]

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