Theorems · Theorem · linear algebra
Matrix.charmatrix_fromBlocks
∀ {R : Type u_1} [inst : CommRing R] {m : Type u_3} {n : Type u_4} [inst_1 : DecidableEq m] [inst_2 : DecidableEq n]
[inst_3 : Fintype m] [inst_4 : Fintype n] (M₁₁ : Matrix m m R) (M₁₂ : Matrix m n R) (M₂₁ : Matrix n m R)
(M₂₂ : Matrix n n R),
(Matrix.fromBlocks M₁₁ M₁₂ M₂₁ M₂₂).charmatrix =
Matrix.fromBlocks M₁₁.charmatrix (-M₁₂.map ⇑Polynomial.C) (-M₂₁.map ⇑Polynomial.C) M₂₂.charmatrix- Cited by
- 2 results in Mathlib
- Foundations
- Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites19
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
- Polynomial.Xproof · cited by 1,639
- Polynomial.Cstatement and proof · cited by 1,598
- Polynomial.coeffproof · cited by 1,045
- Matrix.extproof · cited by 540
- Matrix.ofproof · cited by 336
- zero_subproof · cited by 335
Cited by2
Results whose statement or proof uses this declaration.
- Matrix.charpoly_fromBlocks_zero₁₂proof · cited by 1
- Matrix.charpoly_fromBlocks_zero₂₁proof · cited by 0