fixpointPolynomial_eq_zero_iff — Mathlib

English

The fixed-point polynomial is identically zero if and only if g is a scalar matrix.

Русский

Фиксpoint-полином идентичен нулю тогда и только тогда, когда g скалярная матрица.

LaTeX

$$$g.{\text{fixpointPolynomial}} = 0 \iff g.\text{val} \in \mathrm{range}(\text{scalar} _) $$$

Lean4

/-- The fixed-point polynomial is identically zero iff `g` is scalar. -/
theorem fixpointPolynomial_eq_zero_iff {g : GL (Fin 2) R} : g.fixpointPolynomial = 0 ↔ g.val ∈ Set.range (scalar _) :=
  by
  rw [fixpointPolynomial]
  constructor
  · refine fun hP ↦ ⟨g 0 0, ?_⟩
    have hb : g 0 1 = 0 := by simpa using congr_arg (coeff · 0) hP
    have hc : g 1 0 = 0 := by simpa using congr_arg (coeff · 2) hP
    have hd : g 1 1 = g 0 0 := by simpa [sub_eq_zero] using congr_arg (coeff · 1) hP
    ext i j
    fin_cases i <;> fin_cases j <;> simp [hb, hc, hd]
  · rintro ⟨a, ha⟩
    simp [← ha]

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