Mathlib Map

Theorems · Theorem · group theory

Matrix.isHyperbolic_neg_iff

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Preorder R] {m : Matrix (Fin 2) (Fin 2) R},
  (-m).IsHyperbolic ↔ m.IsHyperbolic
Defined in
Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Cited by
2 results in Mathlib
Foundations
Depth 130 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CommRingPreorder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Matrix.IsHyperbolic.neg · cited by 0IsHyperbolic.negMatrix.IsHyperbolic.of_neg · cited by 0IsHyperbolic.of_negCommRing · cited by 17173CommRingPreorder · cited by 7952PreorderMatrix · cited by 4303Matrixone_mul · cited by 2841one_mulMatrix.det · cited by 665Matrix.detone_pow · cited by 521one_powFintype.card_fin · cited by 270Fintype.card_finMatrix.trace · cited by 114Matrix.traceEven.neg_pow · cited by 99Even.neg_powMatrix.det_neg · cited by 14Matrix.det_negMatrix.discr_fin_two · cited by 12Matrix.discr_fin_twoMatrix.IsHyperbolic · cited by 5Matrix.IsHyperbolicMatrix.trace_neg · cited by 4Matrix.trace_negMatrix.isHyperbolic_neg_iffCITED BYCITES

Cites13

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

Cited by2

Results whose statement or proof uses this declaration.