Theorems · Theorem · linear algebra

Matrix.charpoly_of_card_eq_two

∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R)
  [Nontrivial R],
  Fintype.card n = 2 → M.charpoly = Polynomial.X ^ 2 - Polynomial.C M.trace * Polynomial.X + Polynomial.C M.det

Defined in: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Cited by: 2 results in Mathlib
Foundations: Depth 127 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing DecidableEq Fintype Nontrivial

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites47

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
CommRingstatement and proof · cited by 17,173
RingHomstatement · cited by 10,189
Fintypestatement and proof · cited by 7,736
Polynomialstatement · cited by 5,681
Matrixstatement and proof · cited by 4,303
one_mulproof · cited by 2,841
add_zeroproof · cited by 2,707
Nontrivialstatement and proof · cited by 2,416
zero_addproof · cited by 2,366
MulZeroClass.mul_zeroproof · cited by 2,091
Polynomial.Xstatement and proof · cited by 1,639

Cited by2

Results whose statement or proof uses this declaration.

Matrix.discr_of_card_eq_twoproof · cited by 1
Matrix.charpoly_fin_twoproof · cited by 0