Notation

📁 Source: Mathlib/LinearAlgebra/Matrix/Notation.lean

Statistics

Metric	Count
Definitions `delabMatrixNotation`, `matrixNotation`, `matrixNotation0xC`, `matrixNotationRx0`, `mkLiteralQ`, `repr`, `toExpr`	7
Theorems `cons_dotProduct`, `cons_dotProduct_cons`, `cons_mul`, `cons_mulVec`, `cons_transpose`, `cons_val'`, `cons_vecMul`, `cons_vecMulVec`, `cons_vecMul_cons`, `diagonal_fin_one`, `diagonal_fin_three`, `diagonal_fin_two`, `diagonal_vec1`, `diagonal_vec2`, `diagonal_vec3`, `dotProduct_cons`, `dotProduct_empty`, `dotProduct_of_isEmpty`, `empty_mul`, `empty_mulVec`, `empty_mul_empty`, `empty_vecMul`, `empty_vecMulVec`, `eta_fin_three`, `eta_fin_two`, `head_transpose`, `head_val'`, `mulVec_cons`, `mulVec_empty`, `mul_empty`, `mul_fin_three`, `mul_fin_two`, `mul_val_succ`, `natCast_fin_three`, `natCast_fin_two`, `ofNat_fin_three`, `ofNat_fin_two`, `one_fin_three`, `one_fin_two`, `replicateCol_cons`, `replicateCol_empty`, `replicateRow_cons`, `replicateRow_empty`, `smul_mat_cons`, `smul_mat_empty`, `smul_vec2`, `smul_vec3`, `submatrix_cons_row`, `submatrix_empty`, `submatrix_updateCol_succAbove`, `submatrix_updateRow_succAbove`, `tail_transpose`, `tail_val'`, `transpose_empty_cols`, `transpose_empty_rows`, `vec2_add`, `vec2_dotProduct`, `vec2_dotProduct'`, `vec2_eq`, `vec3_add`, `vec3_dotProduct`, `vec3_dotProduct'`, `vec3_eq`, `vecMulVec_cons`, `vecMulVec_empty`, `vecMul_cons`, `vecMul_empty`, `injective_pair_iff_ne`	68
Total	75

Matrix

Definitions

Name	Category	Theorems
`delabMatrixNotation` 📖	CompOp	—
`matrixNotation` 📖	CompOp	—
`matrixNotation0xC` 📖	CompOp	—
`matrixNotationRx0` 📖	CompOp	—
`mkLiteralQ` 📖	CompOp	—
`repr` 📖	CompOp	—
`toExpr` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cons_dotProduct` 📖	mathematical	—	`dotProduct` `Fin.fintype` `vecCons` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `vecHead` `vecTail`	—	`Fin.sum_univ_succ` `Finset.sum_congr` `cons_val_succ`
`cons_dotProduct_cons` 📖	mathematical	—	`dotProduct` `Fin.fintype` `vecCons` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`dotProduct_cons` `tail_cons`
`cons_mul` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecCons` `vecMul` `Equiv.symm`	—	`ext` `Equiv.symm_apply_apply` `tail_cons` `cons_val'` `cons_val_succ`
`cons_mulVec` 📖	mathematical	—	`mulVec` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecCons` `dotProduct` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`cons_val'` `cons_val_succ`
`cons_transpose` 📖	mathematical	—	`transpose` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecCons`	—	`ext` `cons_val'` `cons_val_succ`
`cons_val'` 📖	mathematical	—	`vecCons`	—	`cons_val_succ`
`cons_vecMul` 📖	mathematical	—	`vecMul` `Fin.fintype` `vecCons` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `instDistribSMul` `vecHead` `vecTail`	—	`cons_dotProduct`
`cons_vecMulVec` 📖	mathematical	—	`vecMulVec` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `vecCons` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `instDistribSMul`	—	`ext` `cons_val'` `cons_val_succ`
`cons_vecMul_cons` 📖	mathematical	—	`vecMul` `Fin.fintype` `vecCons` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `instDistribSMul`	—	`vecMul_cons` `tail_cons`
`diagonal_fin_one` 📖	mathematical	—	`diagonal` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecCons` `vecEmpty`	—	`cons_val'` `cons_val_fin_one` `diagonal_apply_eq`
`diagonal_fin_three` 📖	mathematical	—	`diagonal` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecCons` `vecEmpty`	—	`cons_val'` `cons_val_fin_one` `cons_val_succ` `Fin.isEmpty'` `diagonal_apply_eq` `diagonal_apply_ne` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat`
`diagonal_fin_two` 📖	mathematical	—	`diagonal` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecCons` `vecEmpty`	—	`cons_val'` `cons_val_fin_one` `diagonal_apply_eq` `diagonal_apply_ne` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat`
`diagonal_vec1` 📖	mathematical	—	`diagonal` `vecCons` `vecEmpty` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of`	—	`diagonal_fin_one`
`diagonal_vec2` 📖	mathematical	—	`diagonal` `vecCons` `vecEmpty` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of`	—	`diagonal_fin_two`
`diagonal_vec3` 📖	mathematical	—	`diagonal` `vecCons` `vecEmpty` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of`	—	`diagonal_fin_three`
`dotProduct_cons` 📖	mathematical	—	`dotProduct` `Fin.fintype` `vecCons` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `vecHead` `vecTail`	—	`Fin.sum_univ_succ` `Finset.sum_congr` `cons_val_succ`
`dotProduct_empty` 📖	mathematical	—	`dotProduct` `Fin.fintype` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`Finset.sum_empty`
`dotProduct_of_isEmpty` 📖	mathematical	—	`dotProduct` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`Finset.sum_of_isEmpty`
`empty_mul` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecEmpty`	—	`empty_eq`
`empty_mulVec` 📖	mathematical	—	`mulVec` `vecEmpty`	—	`empty_eq`
`empty_mul_empty` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Fin.fintype` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`empty_vecMul` 📖	mathematical	—	`vecMul` `Fin.fintype` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`empty_vecMulVec` 📖	mathematical	—	`vecMulVec` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `vecEmpty`	—	`empty_eq`
`eta_fin_three` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecCons` `vecEmpty`	—	`ext` `Fintype.complete`
`eta_fin_two` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecCons` `vecEmpty`	—	`ext` `Fintype.complete`
`head_transpose` 📖	mathematical	—	`vecHead` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `of` `transpose`	—	—
`head_val'` 📖	mathematical	—	`vecHead`	—	—
`mulVec_cons` 📖	mathematical	—	`mulVec` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `Fin.fintype` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecCons` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `instDistribSMul` `vecHead` `vecTail`	—	`dotProduct_cons` `mul_comm`
`mulVec_empty` 📖	mathematical	—	`mulVec` `Fin.fintype` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`mul_empty` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecEmpty`	—	`empty_eq`
`mul_fin_three` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Fin.fintype` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecCons` `vecEmpty` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`ext` `Fintype.complete` `Finset.sum_congr` `cons_val'` `cons_val_fin_one` `Fin.sum_univ_succ` `cons_val_succ` `Finset.univ_unique` `Finset.sum_const` `Finset.card_singleton` `one_smul`
`mul_fin_two` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Fin.fintype` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecCons` `vecEmpty` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`ext` `Fintype.complete` `Finset.sum_congr` `cons_val'` `cons_val_fin_one` `Fin.sum_univ_succ` `Finset.univ_unique` `cons_val_succ` `Finset.sum_const` `Finset.card_singleton` `one_smul`
`mul_val_succ` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecTail` `Equiv.symm`	—	—
`natCast_fin_three` 📖	mathematical	—	`Matrix` `instNatCastOfZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddMonoidWithOne.toNatCast` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecCons` `vecEmpty`	—	`ext` `Fintype.complete`
`natCast_fin_two` 📖	mathematical	—	`Matrix` `instNatCastOfZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddMonoidWithOne.toNatCast` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecCons` `vecEmpty`	—	`ext` `Fintype.complete`
`ofNat_fin_three` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecCons` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `vecEmpty`	—	`natCast_fin_three`
`ofNat_fin_two` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecCons` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `vecEmpty`	—	`natCast_fin_two`
`one_fin_three` 📖	mathematical	—	`Matrix` `one` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecCons` `vecEmpty`	—	`ext` `Fintype.complete`
`one_fin_two` 📖	mathematical	—	`Matrix` `one` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecCons` `vecEmpty`	—	`ext` `Fintype.complete`
`replicateCol_cons` 📖	mathematical	—	`replicateCol` `vecCons` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of`	—	`ext` `cons_val'` `cons_val_succ`
`replicateCol_empty` 📖	mathematical	—	`replicateCol` `vecEmpty`	—	`empty_eq`
`replicateRow_cons` 📖	mathematical	—	`replicateRow` `vecCons` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of`	—	—
`replicateRow_empty` 📖	mathematical	—	`replicateRow` `vecEmpty` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of`	—	—
`smul_mat_cons` 📖	mathematical	—	`Pi.instSMul` `vecCons`	—	`smul_cons`
`smul_mat_empty` 📖	mathematical	—	`Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `instDistribSMul` `vecEmpty`	—	`empty_eq`
`smul_vec2` 📖	mathematical	—	`Function.hasSMul` `vecCons` `vecEmpty`	—	`smul_cons` `smul_empty`
`smul_vec3` 📖	mathematical	—	`Function.hasSMul` `vecCons` `vecEmpty`	—	`smul_cons` `smul_empty`
`submatrix_cons_row` 📖	mathematical	—	`submatrix` `vecCons`	—	`ext` `cons_val'` `cons_val_succ`
`submatrix_empty` 📖	mathematical	—	`submatrix` `vecEmpty`	—	`empty_eq`
`submatrix_updateCol_succAbove` 📖	mathematical	—	`submatrix` `updateCol` `Fin.succAbove`	—	`ext` `updateCol_ne` `Fin.succAbove_ne`
`submatrix_updateRow_succAbove` 📖	mathematical	—	`submatrix` `updateRow` `Fin.succAbove`	—	`ext` `updateRow_ne` `Fin.succAbove_ne`
`tail_transpose` 📖	mathematical	—	`vecTail` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `of` `transpose`	—	—
`tail_val'` 📖	mathematical	—	`vecTail`	—	—
`transpose_empty_cols` 📖	mathematical	—	`transpose` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecEmpty`	—	`empty_eq`
`transpose_empty_rows` 📖	mathematical	—	`transpose` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecEmpty`	—	`empty_eq`
`vec2_add` 📖	mathematical	—	`Pi.instAdd` `vecCons` `vecEmpty`	—	`add_cons` `tail_cons` `empty_add_empty`
`vec2_dotProduct` 📖	mathematical	—	`dotProduct` `Fin.fintype` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`vec2_dotProduct'`
`vec2_dotProduct'` 📖	mathematical	—	`dotProduct` `Fin.fintype` `vecCons` `vecEmpty` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`dotProduct_cons` `tail_cons` `dotProduct_of_isEmpty` `Fin.isEmpty'` `add_zero`
`vec2_eq` 📖	mathematical	—	`vecCons` `vecEmpty`	—	—
`vec3_add` 📖	mathematical	—	`Pi.instAdd` `vecCons` `vecEmpty`	—	`add_cons` `tail_cons` `empty_add_empty`
`vec3_dotProduct` 📖	mathematical	—	`dotProduct` `Fin.fintype` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`vec3_dotProduct'`
`vec3_dotProduct'` 📖	mathematical	—	`dotProduct` `Fin.fintype` `vecCons` `vecEmpty` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`dotProduct_cons` `tail_cons` `dotProduct_of_isEmpty` `Fin.isEmpty'` `add_zero` `add_assoc`
`vec3_eq` 📖	mathematical	—	`vecCons` `vecEmpty`	—	—
`vecMulVec_cons` 📖	mathematical	—	`vecMulVec` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `vecCons` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `instDistribSMul`	—	—
`vecMulVec_empty` 📖	mathematical	—	`vecMulVec` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecEmpty`	—	`empty_eq`
`vecMul_cons` 📖	mathematical	—	`vecMul` `Fin.fintype` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `vecCons` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `instDistribSMul` `vecHead` `vecTail`	—	`cons_val'` `dotProduct_cons`
`vecMul_empty` 📖	mathematical	—	`vecMul` `vecEmpty`	—	`empty_eq`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`injective_pair_iff_ne` 📖	mathematical	—	`Matrix.vecCons` `Matrix.vecEmpty`	—	`Matrix.cons_val_fin_one` `Fintype.complete` `zero_add` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat`

---

← Back to Index