RowCol

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

Statistics

Metric	Count
Definitions `replicateCol`, `replicateRow`, `updateCol`, `updateRow`	4
Theorems `conjTranspose_replicateCol`, `conjTranspose_replicateRow`, `diag_replicateCol_mul_replicateRow`, `diagonal_updateCol_single`, `diagonal_updateRow_single`, `map_updateCol`, `map_updateRow`, `mulVec_replicateCol_eq_const`, `mul_single_eq_updateCol_zero`, `mul_updateCol`, `one_vecMulVec`, `reindex_updateCol`, `reindex_updateRow`, `replicateCol_add`, `replicateCol_apply`, `replicateCol_eq_zero`, `replicateCol_inj`, `replicateCol_injective`, `replicateCol_mulVec`, `replicateCol_smul`, `replicateCol_vecMul`, `replicateCol_zero`, `replicateRow_add`, `replicateRow_apply`, `replicateRow_eq_zero`, `replicateRow_inj`, `replicateRow_injective`, `replicateRow_mulVec`, `replicateRow_mulVec_eq_const`, `replicateRow_mul_replicateCol`, `replicateRow_mul_replicateCol_apply`, `replicateRow_smul`, `replicateRow_vecMul`, `replicateRow_zero`, `single_eq_updateCol_zero`, `single_eq_updateRow_zero`, `single_mul_eq_updateRow_zero`, `submatrix_updateCol_equiv`, `submatrix_updateRow_equiv`, `transpose_replicateCol`, `transpose_replicateRow`, `updateCol_apply`, `updateCol_comm`, `updateCol_conjTranspose`, `updateCol_eq_self`, `updateCol_idem`, `updateCol_ne`, `updateCol_reindex`, `updateCol_self`, `updateCol_submatrix_equiv`, `updateCol_subsingleton`, `updateCol_transpose`, `updateCol_zero_zero`, `updateRow_apply`, `updateRow_comm`, `updateRow_conjTranspose`, `updateRow_eq_self`, `updateRow_idem`, `updateRow_mul`, `updateRow_mulVec`, `updateRow_ne`, `updateRow_reindex`, `updateRow_self`, `updateRow_submatrix_equiv`, `updateRow_subsingleton`, `updateRow_transpose`, `updateRow_zero_mul_updateCol_zero`, `updateRow_zero_zero`, `update_vecMulVec`, `vecMulVec_eq`, `vecMulVec_one`, `vecMulVec_update`, `vecMul_updateCol`	73
Total	77

Matrix

Definitions

Name	Category	Theorems
`replicateCol` 📖	CompOp	34 math math: `frobenius_norm_replicateCol`, `replicateCol_empty`, `replicateCol_zero`, `replicateCol_cons`, `replicateCol_injective`, `det_add_replicateCol_mul_replicateRow`, `replicateRow_mulVec`, `Continuous.matrix_replicateCol`, `diag_replicateCol_mul_replicateRow`, `transpose_replicateCol`, `fromCols_replicateCol0_isTotallyUnimodular_iff`, `conjTranspose_replicateRow`, `vecMulVec_eq`, `trace_replicateCol_mul_replicateRow`, `mulVec_replicateCol_eq_const`, `replicateCol_mulVec`, `replicateRow_mul_replicateCol`, `frobenius_nnnorm_replicateCol`, `vecMulVec_one`, `linfty_opNorm_replicateCol`, `replicateCol_smul`, `linfty_opNNNorm_replicateCol`, `replicateCol_eq_zero`, `det_one_add_replicateCol_mul_replicateRow`, `replicateRow_mul_replicateCol_apply`, `updateCol_subsingleton`, `replicateCol_vecMul`, `transpose_replicateRow`, `replicateCol_apply`, `norm_replicateCol`, `replicateCol_inj`, `conjTranspose_replicateCol`, `nnnorm_replicateCol`, `replicateCol_add`
`replicateRow` 📖	CompOp	34 math math: `det_add_replicateCol_mul_replicateRow`, `replicateRow_mulVec`, `replicateRow_zero`, `linfty_opNorm_replicateRow`, `diag_replicateCol_mul_replicateRow`, `transpose_replicateCol`, `replicateRow_inj`, `replicateRow_empty`, `replicateRow_cons`, `replicateRow_mulVec_eq_const`, `conjTranspose_replicateRow`, `replicateRow_add`, `vecMulVec_eq`, `one_vecMulVec`, `trace_replicateCol_mul_replicateRow`, `nnnorm_replicateRow`, `replicateRow_eq_zero`, `norm_replicateRow`, `frobenius_nnnorm_replicateRow`, `replicateRow_mul_replicateCol`, `Continuous.matrix_replicateRow`, `replicateRow_vecMul`, `fromRows_replicateRow0_isTotallyUnimodular_iff`, `replicateRow_apply`, `det_one_add_replicateCol_mul_replicateRow`, `replicateRow_mul_replicateCol_apply`, `replicateCol_vecMul`, `updateRow_subsingleton`, `transpose_replicateRow`, `linfty_opNNNorm_replicateRow`, `replicateRow_smul`, `frobenius_norm_replicateRow`, `conjTranspose_replicateCol`, `replicateRow_injective`
`updateCol` 📖	CompOp	36 math math: `det_updateCol_eq_zero`, `updateCol_self`, `updateCol_reindex`, `updateCol_apply`, `vecMulVec_update`, `updateRow_transpose`, `cramer_apply`, `mul_updateCol`, `det_updateCol_add`, `submatrix_updateCol_equiv`, `permanent_updateCol_smul`, `updateCol_ne`, `diagonal_updateCol_single`, `mul_single_eq_updateCol_zero`, `Continuous.matrix_updateCol`, `updateCol_comm`, `updateCol_submatrix_equiv`, `det_updateCol_smul`, `det_updateCol_sum`, `Module.Basis.toMatrix_update`, `updateCol_zero_zero`, `det_updateCol_add_smul_self`, `updateCol_conjTranspose`, `updateRow_zero_mul_updateCol_zero`, `single_eq_updateCol_zero`, `updateCol_subsingleton`, `det_updateCol_add_self`, `updateCol_eq_self`, `map_updateCol`, `vecMul_updateCol`, `updateRow_conjTranspose`, `updateCol_idem`, `updateCol_transpose`, `det_updateCol_smul_left`, `reindex_updateCol`, `submatrix_updateCol_succAbove`
`updateRow` 📖	CompOp	39 math math: `single_eq_updateRow_zero`, `det_updateRow_add_self`, `updateRow_mul`, `det_updateRow_add_smul_self`, `diagonal_updateRow_single`, `det_updateRow_smul_left`, `updateRow_eq_transvection`, `updateRow_submatrix_equiv`, `updateRow_transpose`, `permanent_updateRow_smul`, `det_updateRow_sum_aux`, `map_updateRow`, `submatrix_updateRow_succAbove`, `updateRow_reindex`, `updateRow_idem`, `det_updateRow_sum`, `adjugate_apply`, `updateRow_ne`, `updateRow_comm`, `reindex_updateRow`, `submatrix_updateRow_equiv`, `Polynomial.sylvesterDeriv_updateRow`, `single_mul_eq_updateRow_zero`, `det_updateRow_eq_zero`, `update_vecMulVec`, `updateCol_conjTranspose`, `updateRow_eq_self`, `updateRow_zero_mul_updateCol_zero`, `det_updateRow_smul`, `updateRow_self`, `updateRow_mulVec`, `updateRow_subsingleton`, `updateRow_conjTranspose`, `updateCol_transpose`, `cramer_transpose_apply`, `det_updateRow_add`, `updateRow_zero_zero`, `updateRow_apply`, `Continuous.matrix_updateRow`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conjTranspose_replicateCol` 📖	mathematical	—	`conjTranspose` `replicateCol` `replicateRow` `Star.star` `Pi.instStarForall`	—	`ext`
`conjTranspose_replicateRow` 📖	mathematical	—	`conjTranspose` `replicateRow` `replicateCol` `Star.star` `Pi.instStarForall`	—	`ext`
`diag_replicateCol_mul_replicateRow` 📖	mathematical	—	`diag` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Unique.fintype` `replicateCol` `replicateRow` `Pi.instMul`	—	`Finset.sum_congr` `Finset.univ_unique` `Finset.sum_const` `Finset.card_singleton` `one_smul`
`diagonal_updateCol_single` 📖	mathematical	—	`updateCol` `diagonal` `Pi.single` `Function.update`	—	`ext` `eq_or_ne` `diagonal_apply_eq` `updateCol_self` `Pi.single_eq_same` `Function.update_self` `updateCol_ne` `Function.update_of_ne` `diagonal_apply_ne` `Pi.single_eq_of_ne`
`diagonal_updateRow_single` 📖	mathematical	—	`updateRow` `diagonal` `Pi.single` `Function.update`	—	`diagonal_transpose` `updateRow_transpose` `diagonal_updateCol_single`
`map_updateCol` 📖	mathematical	—	`map` `updateCol`	—	`ext` `updateCol_apply` `map_apply`
`map_updateRow` 📖	mathematical	—	`map` `updateRow`	—	`ext` `updateRow_apply` `map_apply`
`mulVec_replicateCol_eq_const` 📖	mathematical	—	`vecMul` `replicateCol` `dotProduct` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	—
`mul_single_eq_updateCol_zero` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid` `single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `updateCol` `zero` `MulOpposite` `Function.hasSMul` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `MulOpposite.instZero` `MulZeroClass.toOppositeSMulWithZero` `MulOpposite.op` `col`	—	`single_eq_updateCol_zero` `mul_updateCol` `mul_zero` `mulVec_single`
`mul_updateCol` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid` `updateCol` `mulVec`	—	`ext` `eq_or_ne` `Finset.sum_congr` `updateCol_self` `updateCol_ne`
`one_vecMulVec` 📖	mathematical	—	`vecMulVec` `MulOne.toMul` `MulOneClass.toMulOne` `Pi.instOne` `MulOne.toOne` `replicateRow`	—	`ext` `one_mul`
`reindex_updateCol` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex` `updateCol` `Equiv.symm`	—	`submatrix_updateCol_equiv`
`reindex_updateRow` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex` `updateRow` `Equiv.symm`	—	`submatrix_updateRow_equiv`
`replicateCol_add` 📖	mathematical	—	`replicateCol` `Pi.instAdd` `Matrix` `add`	—	`ext`
`replicateCol_apply` 📖	mathematical	—	`replicateCol`	—	—
`replicateCol_eq_zero` 📖	mathematical	—	`replicateCol` `Matrix` `zero` `Pi.instZero`	—	—
`replicateCol_inj` 📖	mathematical	—	`replicateCol`	—	`replicateCol_injective`
`replicateCol_injective` 📖	mathematical	—	`Matrix` `replicateCol`	—	—
`replicateCol_mulVec` 📖	mathematical	—	`replicateCol` `mulVec` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`ext`
`replicateCol_smul` 📖	mathematical	—	`replicateCol` `Function.hasSMul` `Matrix` `smul`	—	`ext`
`replicateCol_vecMul` 📖	mathematical	—	`replicateCol` `vecMul` `transpose` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid` `replicateRow`	—	`ext`
`replicateCol_zero` 📖	mathematical	—	`replicateCol` `Pi.instZero` `Matrix` `zero`	—	—
`replicateRow_add` 📖	mathematical	—	`replicateRow` `Pi.instAdd` `Matrix` `add`	—	`ext`
`replicateRow_apply` 📖	mathematical	—	`replicateRow`	—	—
`replicateRow_eq_zero` 📖	mathematical	—	`replicateRow` `Matrix` `zero` `Pi.instZero`	—	—
`replicateRow_inj` 📖	mathematical	—	`replicateRow`	—	`replicateRow_injective`
`replicateRow_injective` 📖	mathematical	—	`Matrix` `replicateRow`	—	—
`replicateRow_mulVec` 📖	mathematical	—	`replicateRow` `mulVec` `transpose` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid` `replicateCol`	—	`ext`
`replicateRow_mulVec_eq_const` 📖	mathematical	—	`mulVec` `replicateRow` `dotProduct` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	—
`replicateRow_mul_replicateCol` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `replicateRow` `replicateCol` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `dotProduct`	—	—
`replicateRow_mul_replicateCol_apply` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `replicateRow` `replicateCol` `dotProduct`	—	—
`replicateRow_smul` 📖	mathematical	—	`replicateRow` `Function.hasSMul` `Matrix` `smul`	—	`ext`
`replicateRow_vecMul` 📖	mathematical	—	`replicateRow` `vecMul` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`ext`
`replicateRow_zero` 📖	mathematical	—	`replicateRow` `Pi.instZero` `Matrix` `zero`	—	—
`single_eq_updateCol_zero` 📖	mathematical	—	`single` `updateCol` `Matrix` `zero` `Pi.single`	—	`transpose_single` `single_eq_updateRow_zero`
`single_eq_updateRow_zero` 📖	mathematical	—	`single` `updateRow` `Matrix` `zero` `Pi.single`	—	`single_eq_of_single_single`
`single_mul_eq_updateRow_zero` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid` `single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `updateRow` `zero` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `instDistribSMul` `row`	—	`single_eq_updateRow_zero` `updateRow_mul` `zero_mul` `single_vecMul`
`submatrix_updateCol_equiv` 📖	mathematical	—	`submatrix` `updateCol` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	`Equiv.apply_symm_apply` `updateCol_submatrix_equiv`
`submatrix_updateRow_equiv` 📖	mathematical	—	`submatrix` `updateRow` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	`Equiv.apply_symm_apply` `updateRow_submatrix_equiv`
`transpose_replicateCol` 📖	mathematical	—	`transpose` `replicateCol` `replicateRow`	—	`ext`
`transpose_replicateRow` 📖	mathematical	—	`transpose` `replicateRow` `replicateCol`	—	`ext`
`updateCol_apply` 📖	mathematical	—	`updateCol`	—	`updateCol_self` `updateCol_ne`
`updateCol_comm` 📖	mathematical	—	`updateCol`	—	`updateRow_transpose` `updateRow_comm`
`updateCol_conjTranspose` 📖	mathematical	—	`updateCol` `conjTranspose` `Star.star` `Pi.instStarForall` `updateRow`	—	`conjTranspose.eq_1` `transpose_map` `updateCol_transpose` `map_updateRow`
`updateCol_eq_self` 📖	mathematical	—	`updateCol`	—	`Function.update_eq_self`
`updateCol_idem` 📖	mathematical	—	`updateCol`	—	`updateRow_transpose` `updateRow_idem`
`updateCol_ne` 📖	mathematical	—	`updateCol`	—	`Function.update_of_ne`
`updateCol_reindex` 📖	mathematical	—	`updateCol` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex` `Equiv.symm`	—	`updateCol_submatrix_equiv`
`updateCol_self` 📖	mathematical	—	`updateCol`	—	`Function.update_self`
`updateCol_submatrix_equiv` 📖	mathematical	—	`updateCol` `submatrix` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	`updateRow_transpose` `updateRow_submatrix_equiv`
`updateCol_subsingleton` 📖	mathematical	—	`updateCol` `decidableEq_of_subsingleton` `submatrix` `replicateCol`	—	`ext` `updateCol.congr_simp` `updateCol_self`
`updateCol_transpose` 📖	mathematical	—	`updateCol` `transpose` `updateRow`	—	`ext` `transpose_apply` `updateRow_apply` `updateCol_apply`
`updateCol_zero_zero` 📖	mathematical	—	`updateCol` `Matrix` `zero` `Pi.instZero`	—	`updateCol_eq_self`
`updateRow_apply` 📖	mathematical	—	`updateRow`	—	`updateRow_self` `updateRow_ne`
`updateRow_comm` 📖	mathematical	—	`updateRow`	—	`Function.update_comm`
`updateRow_conjTranspose` 📖	mathematical	—	`updateRow` `conjTranspose` `Star.star` `Pi.instStarForall` `updateCol`	—	`conjTranspose.eq_1` `transpose_map` `updateRow_transpose` `map_updateCol`
`updateRow_eq_self` 📖	mathematical	—	`updateRow`	—	`Function.update_eq_self`
`updateRow_idem` 📖	mathematical	—	`updateRow`	—	`Function.update_idem`
`updateRow_mul` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid` `updateRow` `vecMul`	—	`ext` `eq_or_ne` `Finset.sum_congr` `updateRow_self` `updateRow_ne`
`updateRow_mulVec` 📖	mathematical	—	`mulVec` `updateRow` `Function.update` `dotProduct` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`eq_or_ne` `updateRow_self` `Function.update_self` `updateRow_ne` `Function.update_of_ne`
`updateRow_ne` 📖	mathematical	—	`updateRow`	—	`Function.update_of_ne`
`updateRow_reindex` 📖	mathematical	—	`updateRow` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex` `Equiv.symm`	—	`updateRow_submatrix_equiv`
`updateRow_self` 📖	mathematical	—	`updateRow`	—	`Function.update_self`
`updateRow_submatrix_equiv` 📖	mathematical	—	`updateRow` `submatrix` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	`ext` `updateRow_apply` `Equiv.symm_apply_apply`
`updateRow_subsingleton` 📖	mathematical	—	`updateRow` `decidableEq_of_subsingleton` `submatrix` `replicateRow`	—	`ext` `updateRow.congr_simp` `updateRow_self`
`updateRow_transpose` 📖	mathematical	—	`updateRow` `transpose` `updateCol`	—	`ext` `transpose_apply` `updateRow_apply` `updateCol_apply`
`updateRow_zero_mul_updateCol_zero` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid` `updateRow` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `updateCol` `single` `dotProduct`	—	`updateRow_mul` `vecMul_updateCol` `mul_updateCol` `single_eq_of_single_single` `zero_mul` `vecMul_zero` `zero_mulVec` `updateCol_zero_zero` `updateRow.eq_1` `Pi.single.eq_1`
`updateRow_zero_zero` 📖	mathematical	—	`updateRow` `Matrix` `zero` `Pi.instZero`	—	`updateRow_eq_self`
`update_vecMulVec` 📖	mathematical	—	`vecMulVec` `Function.update` `updateRow` `Function.hasSMul`	—	`ext` `eq_or_ne` `Function.update_self` `updateRow_self` `Function.update_of_ne` `updateRow_ne`
`vecMulVec_eq` 📖	mathematical	—	`vecMulVec` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Unique.fintype` `replicateCol` `replicateRow`	—	`ext` `Finset.sum_congr` `Finset.univ_unique` `Finset.sum_const` `Finset.card_singleton` `one_smul`
`vecMulVec_one` 📖	mathematical	—	`vecMulVec` `MulOne.toMul` `MulOneClass.toMulOne` `Pi.instOne` `MulOne.toOne` `replicateCol`	—	`ext` `mul_one`
`vecMulVec_update` 📖	mathematical	—	`vecMulVec` `Function.update` `updateCol` `MulOpposite` `Function.hasSMul` `Mul.toSMulMulOpposite` `MulOpposite.op`	—	`ext` `eq_or_ne` `Function.update_self` `updateCol_self` `Function.update_of_ne` `updateCol_ne`
`vecMul_updateCol` 📖	mathematical	—	`vecMul` `updateCol` `Function.update` `dotProduct` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`eq_or_ne` `updateCol_self` `Function.update_self` `updateCol_ne` `Function.update_of_ne`

---

← Back to Index