IsParabolic — Mathlib

English

A 2×2 matrix over a field is parabolic if it is not scalar and its discriminant is zero.

Русский

Матрица размером 2×2 над полем параболична, если она не скалярна и её дискриминант равен нулю.

LaTeX

$$$\text{IsParabolic}(m) \;\iff\; m \text{ non\-scalar} \wedge \operatorname{disc}(m)=0.$$$

Lean4

/-- A `2 × 2` matrix is *parabolic* if it is non-scalar and its discriminant is 0. -/
def IsParabolic : Prop :=
  m ∉ Set.range (scalar _) ∧ m.disc = 0

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