smul_some_eq_ite — Mathlib

English

For any g ∈ GL(2,K) and k ∈ K, g • (k : OnePoint K) equals ∞ if g10 k + g11 = 0, else the finite point corresponding to (g00 k + g01) / (g10 k + g11).

Русский

Для g ∈ GL(2,K) и k ∈ K, g • (k : OnePoint K) равно ∞, если g10 k + g11 = 0, иначе точка [g00 k + g01 : g10 k + g11].

LaTeX

$$$g\\cdot (k:\\mathrm{OnePoint}(K)) = \\begin{cases} \\infty, & g_{10}k+g_{11}=0 \\\\ \\text{OnePoint.some}\\left(\\dfrac{g_{00}k+g_{01}}{g_{10}k+g_{11}}\\right), & \\text{otherwise} \\end{cases}$$$

Lean4

theorem smul_some_eq_ite {g : GL (Fin 2) K} {k : K} :
    g • (k : OnePoint K) = if g 1 0 * k + g 1 1 = 0 then ∞ else (g 0 0 * k + g 0 1) / (g 1 0 * k + g 1 1) := by
  simp [Equiv.smul_def, mulVec_eq_sum, div_eq_inv_mul, mul_comm, Units.smul_def]

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