IsElliptic

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

URI: https://scilib.ai/kg/mathlib#Matrix.GeneralLinearGroup.IsElliptic

English

The elliptic property for GL2 is defined by the ellipticity of the underlying matrix.

Русский

Эллиптическое свойство в GL2 задаётся через эллиптичность лежащей в основе матрицы.

LaTeX

$$$IsElliptic\{GL\}\bigl(g\bigr) \iff g.\text{val}.IsElliptic$$$

Lean4

/-- Synonym of `Matrix.IsElliptic`, for dot-notation. -/
abbrev IsElliptic [Preorder R] (g : GL (Fin 2) R) : Prop :=
  g.val.IsElliptic

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

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

Разделы

Аффилиация

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