disc_of_card_eq_two

Mathlib.LinearAlgebra.Matrix.Charpoly.Disc

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

← MathLib Explorer

English

For a 2×2 matrix A, the discriminant equals trace(A)^2 − 4 det(A).

Русский

Для матрицы размера 2×2 дискриминант равен трейс(A)^2 − 4 det(A).

LaTeX

$$disc(A) = trace(A)^2 - 4 \\det(A)$$

Lean4

theorem disc_of_card_eq_two (A : Matrix n n R) (hn : Fintype.card n = 2) : A.disc = A.trace ^ 2 - 4 * A.det :=
  by
  rw [disc, Polynomial.disc_of_degree_eq_two (by simp; norm_cast)]
  simp [A.charpoly_of_card_eq_two hn]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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