disc_fin_two

Mathlib.LinearAlgebra.Matrix.Charpoly.Disc

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

English

In the 2-point finite case, the discriminant formula holds: A.disc = A.trace^2 − 4 A.det.

Русский

В конечном случае размера два формула дискриминанта сохраняется: A.disc = A.trace^2 − 4 A.det.

LaTeX

$$A.disc = A.trace^2 - 4 * A.det$$

Lean4

theorem disc_fin_two (A : Matrix (Fin 2) (Fin 2) R) : A.disc = A.trace ^ 2 - 4 * A.det :=
  A.disc_of_card_eq_two <| Fintype.card_fin _

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

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

Разделы

Аффилиация

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