Theorems · Theorem · linear algebra
Matrix.commute_diagonal
∀ {n : Type u_3} {α : Type u_10} [inst : NonUnitalNonAssocCommSemiring α] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
(d₁ d₂ : n → α), Commute (Matrix.diagonal d₁) (Matrix.diagonal d₂)- Defined in
- Mathlib.Data.Matrix.Mul
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fintypestatement and proof · cited by 7,736
- Matrixstatement · cited by 4,303
- mul_commproof · cited by 2,262
- Commutestatement · cited by 639
- Matrix.diagonalstatement and proof · cited by 314
- NonUnitalNonAssocCommSemiringstatement and proof · cited by 10
- Matrix.diagonal_mul_diagonalproof · cited by 9
Cited by1
Results whose statement or proof uses this declaration.
- RootPairing.GeckConstruction.lie_h_hproof · cited by 0