IsHyperbolic

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

URI: https://scilib.ai/kg/mathlib#Matrix.IsHyperbolic

English

A 2×2 matrix is hyperbolic if its discriminant is strictly positive: 0 < disc(m).

Русский

Матрица 2×2 гиперболическая, если дискриминант строго положителен: 0 < disc(m).

LaTeX

$$$\text{IsHyperbolic}(m) \iff 0 < \operatorname{disc}(m).$$$

Lean4

/-- A `2 × 2` matrix is *hyperbolic* if its discriminant is strictly positive. -/
def IsHyperbolic : Prop :=
  0 < m.disc

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru