smul_infty_eq_ite — Mathlib

English

For any g ∈ GL(2,K), g • ∞ equals ∞ if g10 = 0, otherwise equals g00 / g10.

Русский

Для любого g ∈ GL(2,K) g • ∞ равно ∞ если g10 = 0, иначе g00 / g10.

LaTeX

$$$g\\cdot \\infty = \\begin{cases} \\infty, & g_{10}=0 \\\\ g_{00}/g_{10}, & g_{10}\\neq 0 \\end{cases}$$$

Lean4

theorem smul_infty_eq_ite (g : GL (Fin 2) K) : g • (∞ : OnePoint K) = if g 1 0 = 0 then ∞ else g 0 0 / g 1 0 := by
  by_cases h : g 1 0 = 0 <;> simp [h, div_eq_inv_mul, smul_infty_def]

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