Mathlib Map

Theorems · Theorem · linear algebra

Matrix.detp.congr_simp

∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] {inst_1 : DecidableEq n} [inst_2 : DecidableEq n]
  [inst_3 : CommSemiring R] (s s_1 : ℤˣ),
  s = s_1 → ∀ (A A_1 : Matrix n n R), A = A_1 → Matrix.detp s A = Matrix.detp s_1 A_1
Defined in
Mathlib.LinearAlgebra.Matrix.SemiringInverse
Cited by
4 results in Mathlib
Foundations
Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
FintypeDecidableEqCommSemiring
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Matrix.Nonsingular.of_linearIndependent_col · cited by 3Nonsingular.of_linearInde…Matrix.adjp_none_none · cited by 1Matrix.adjp_none_noneMatrix.detp_submatrix_equiv_self · cited by 0Matrix.detp_submatrix_equ…Matrix.adjp_none_some · cited by 0Matrix.adjp_none_someCommSemiring · cited by 10911CommSemiringFintype · cited by 7736FintypeMatrix · cited by 4303MatrixUnits · cited by 2804UnitsMatrix.detp · cited by 37Matrix.detpdetp.congr_simpCITED BYCITES

Cites5

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

  • CommSemiringstatement and proof · cited by 10,911
  • Fintypestatement and proof · cited by 7,736
  • Matrixstatement and proof · cited by 4,303
  • Unitsstatement and proof · cited by 2,804
  • Matrix.detpstatement and proof · cited by 37

Cited by4

Results whose statement or proof uses this declaration.