Mathlib Map

Theorems · Definition · group theory

Matrix.parabolicEigenvalue

{K : Type u_1} → [Field K] → Matrix (Fin 2) (Fin 2) K → K

The unique eigenvalue of a parabolic matrix (junk if m is not parabolic).

Defined in
Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Cited by
3 results in Mathlib
Foundations
Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
Field
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Matrix.IsParabolic.sub_eigenvalue_sq_eq_zero · cited by 1IsParabolic.sub_eigenvalu…Matrix.isParabolic_iff_exists · cited by 1Matrix.isParabolic_iff_ex…Matrix.GeneralLinearGroup.parabolicEigenvalue_ne_zero · cited by 0GeneralLinearGroup.parabo…Field · cited by 7404FieldMatrix · cited by 4303MatrixMatrix.trace · cited by 114Matrix.traceMatrix.parabolicEigenvalueCITED BYCITES

Cites3

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

  • Fieldstatement and proof · cited by 7,404
  • Matrixstatement and proof · cited by 4,303
  • Matrix.traceproof · cited by 114

Cited by3

Results whose statement or proof uses this declaration.