Theorems · Theorem · linear algebra

Matrix.TransvectionStruct.toMatrix_sumInl

∀ {n : Type u_1} (p : Type u_2) {R : Type u₂} [inst : DecidableEq n] [inst_1 : DecidableEq p] [inst_2 : CommRing R]
  (t : Matrix.TransvectionStruct n R),
  (Matrix.TransvectionStruct.sumInl p t).toMatrix = Matrix.fromBlocks t.toMatrix 0 0 1

Defined in: Mathlib.LinearAlgebra.Matrix.Transvection
Cited by: 2 results in Mathlib
Foundations: Depth 19 from the axioms · uses propext, Quot.sound
Assumes: DecidableEq DecidableEq CommRing

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites17

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

DFunLike.coeproof · cited by 62,936
CommRingstatement and proof · cited by 17,173
Matrixstatement · cited by 4,303
add_zeroproof · cited by 2,707
zero_addproof · cited by 2,366
Matrix.extproof · cited by 540
Matrix.ofproof · cited by 336
Matrix.singleproof · cited by 129
Matrix.fromBlocksstatement and proof · cited by 108
Matrix.TransvectionStructstatement and proof · cited by 42
Matrix.one_apply_neproof · cited by 39
Matrix.one_apply_eqproof · cited by 35

Cited by2

Results whose statement or proof uses this declaration.

Matrix.TransvectionStruct.mul_sumInl_toMatrix_prodproof · cited by 1
Matrix.TransvectionStruct.sumInl_toMatrix_prod_mulproof · cited by 1