ColumnRowPartitioned

📁 Source: Mathlib/Data/Matrix/ColumnRowPartitioned.lean

Statistics

Metric	Count
Definitions `fromCols`, `fromRows`, `toCols₁`, `toCols₂`, `toRows₁`, `toRows₂`	6
Theorems `conjTranspose_fromCols_eq_fromRows_conjTranspose`, `conjTranspose_fromRows_eq_fromCols_conjTranspose`, `equiv_compl_fromCols_mul_fromRows_eq_one_comm`, `fromBlocks_mul_fromRows`, `fromCols_apply_inl`, `fromCols_apply_inr`, `fromCols_ext_iff`, `fromCols_fromRows_eq_fromBlocks`, `fromCols_inj`, `fromCols_map`, `fromCols_mulVec`, `fromCols_mulVec_sumElim`, `fromCols_mul_fromBlocks`, `fromCols_mul_fromRows`, `fromCols_mul_fromRows_eq_one_comm`, `fromCols_neg`, `fromCols_toCols`, `fromCols_zero`, `fromRows_apply_inl`, `fromRows_apply_inr`, `fromRows_ext_iff`, `fromRows_fromCols_eq_fromBlocks`, `fromRows_inj`, `fromRows_map`, `fromRows_mul`, `fromRows_mulVec`, `fromRows_mul_fromCols`, `fromRows_neg`, `fromRows_toRows`, `fromRows_zero`, `mul_fromCols`, `sumElim_vecMul_fromRows`, `toCols₁_apply`, `toCols₁_fromCols`, `toCols₂_apply`, `toCols₂_fromCols`, `toRows₁_apply`, `toRows₁_fromRows`, `toRows₂_apply`, `toRows₂_fromRows`, `transpose_fromCols`, `transpose_fromRows`, `vecMul_fromCols`, `vecMul_fromRows`	44
Total	50

Matrix

Definitions

Name	Category	Theorems
`fromCols` 📖	CompOp	30 math math: `fromCols_map`, `fromCols_apply_inl`, `fromRows_fromCols_eq_fromBlocks`, `fromCols_ext_iff`, `one_fromCols_isTotallyUnimodular_iff`, `equiv_compl_fromCols_mul_fromRows_eq_one_comm`, `IsTotallyUnimodular.fromCols_one`, `fromCols_replicateCol0_isTotallyUnimodular_iff`, `fromRows_mul_fromCols`, `mul_fromCols`, `toCols₁_fromCols`, `conjTranspose_fromCols_eq_fromRows_conjTranspose`, `conjTranspose_fromRows_eq_fromCols_conjTranspose`, `transpose_fromRows`, `fromCols_mul_fromRows_eq_one_comm`, `vecMul_fromCols`, `IsTotallyUnimodular.one_fromCols`, `transpose_fromCols`, `fromCols_one_isTotallyUnimodular_iff`, `fromCols_toCols`, `fromCols_mulVec_sumElim`, `fromCols_mul_fromRows`, `fromCols_inj`, `toCols₂_fromCols`, `fromCols_neg`, `fromCols_mulVec`, `fromCols_mul_fromBlocks`, `fromCols_zero`, `fromCols_fromRows_eq_fromBlocks`, `fromCols_apply_inr`
`fromRows` 📖	CompOp	32 math math: `fromRows_zero`, `toRows₁_fromRows`, `fromRows_fromCols_eq_fromBlocks`, `vecMul_fromRows`, `one_fromRows_isTotallyUnimodular_iff`, `fromBlocks_mul_fromRows`, `equiv_compl_fromCols_mul_fromRows_eq_one_comm`, `IsTotallyUnimodular.fromRows_unitlike`, `fromRows_neg`, `IsTotallyUnimodular.one_fromRows`, `fromRows_isTotallyUnimodular_iff_rows`, `fromRows_apply_inl`, `fromRows_mul_fromCols`, `fromRows_one_isTotallyUnimodular_iff`, `conjTranspose_fromCols_eq_fromRows_conjTranspose`, `conjTranspose_fromRows_eq_fromCols_conjTranspose`, `fromRows_apply_inr`, `fromRows_toRows`, `transpose_fromRows`, `fromRows_replicateRow0_isTotallyUnimodular_iff`, `fromRows_map`, `fromCols_mul_fromRows_eq_one_comm`, `fromRows_ext_iff`, `sumElim_vecMul_fromRows`, `fromRows_mul`, `transpose_fromCols`, `IsTotallyUnimodular.fromRows_one`, `fromCols_mul_fromRows`, `fromRows_mulVec`, `fromRows_inj`, `toRows₂_fromRows`, `fromCols_fromRows_eq_fromBlocks`
`toCols₁` 📖	CompOp	3 math math: `toCols₁_fromCols`, `toCols₁_apply`, `fromCols_toCols`
`toCols₂` 📖	CompOp	3 math math: `toCols₂_apply`, `fromCols_toCols`, `toCols₂_fromCols`
`toRows₁` 📖	CompOp	3 math math: `toRows₁_fromRows`, `fromRows_toRows`, `toRows₁_apply`
`toRows₂` 📖	CompOp	3 math math: `fromRows_toRows`, `toRows₂_apply`, `toRows₂_fromRows`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conjTranspose_fromCols_eq_fromRows_conjTranspose` 📖	mathematical	—	`conjTranspose` `fromCols` `fromRows`	—	`ext`
`conjTranspose_fromRows_eq_fromCols_conjTranspose` 📖	mathematical	—	`conjTranspose` `fromRows` `fromCols`	—	`ext`
`equiv_compl_fromCols_mul_fromRows_eq_one_comm` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `instFintypeSum` `Subtype.fintype` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `fromCols` `fromRows` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`fromCols_mul_fromRows_eq_one_comm`
`fromBlocks_mul_fromRows` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `instFintypeSum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `fromBlocks` `fromRows` `add` `Distrib.toAdd`	—	`ext` `Fintype.sum_sum_type` `Finset.sum_congr`
`fromCols_apply_inl` 📖	mathematical	—	`fromCols`	—	—
`fromCols_apply_inr` 📖	mathematical	—	`fromCols`	—	—
`fromCols_ext_iff` 📖	mathematical	—	`fromCols`	—	`Function.Injective2.eq_iff`
`fromCols_fromRows_eq_fromBlocks` 📖	mathematical	—	`fromCols` `fromRows` `fromBlocks`	—	`ext`
`fromCols_inj` 📖	mathematical	—	`Function.Injective2` `Matrix` `fromCols`	—	—
`fromCols_map` 📖	mathematical	—	`map` `fromCols`	—	`ext`
`fromCols_mulVec` 📖	mathematical	—	`mulVec` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instFintypeSum` `fromCols` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`fromCols_mulVec_sumElim` 📖	mathematical	—	`mulVec` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instFintypeSum` `fromCols` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	`sumElim_dotProduct_sumElim`
`fromCols_mul_fromBlocks` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `instFintypeSum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `fromCols` `fromBlocks` `add` `Distrib.toAdd`	—	`ext` `Fintype.sum_sum_type` `Finset.sum_congr`
`fromCols_mul_fromRows` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `instFintypeSum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `fromCols` `fromRows` `add` `Distrib.toAdd`	—	`ext` `Fintype.sum_sum_type` `Finset.sum_congr`
`fromCols_mul_fromRows_eq_one_comm` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `instFintypeSum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `fromCols` `fromRows` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`mul_eq_one_comm_of_equiv` `instIsStablyFiniteRingOfCommSemiring`
`fromCols_neg` 📖	mathematical	—	`Matrix` `neg` `fromCols`	—	`ext`
`fromCols_toCols` 📖	mathematical	—	`fromCols` `toCols₁` `toCols₂`	—	`ext`
`fromCols_zero` 📖	mathematical	—	`fromCols` `Matrix` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`ext`
`fromRows_apply_inl` 📖	mathematical	—	`fromRows`	—	—
`fromRows_apply_inr` 📖	mathematical	—	`fromRows`	—	—
`fromRows_ext_iff` 📖	mathematical	—	`fromRows`	—	`Function.Injective2.eq_iff`
`fromRows_fromCols_eq_fromBlocks` 📖	mathematical	—	`fromRows` `fromCols` `fromBlocks`	—	`ext`
`fromRows_inj` 📖	mathematical	—	`Function.Injective2` `Matrix` `fromRows`	—	—
`fromRows_map` 📖	mathematical	—	`map` `fromRows`	—	`ext`
`fromRows_mul` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `fromRows`	—	`ext` `Finset.sum_congr`
`fromRows_mulVec` 📖	mathematical	—	`mulVec` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `fromRows`	—	—
`fromRows_mul_fromCols` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `fromRows` `fromCols` `fromBlocks`	—	`ext` `mul_fromCols` `fromRows_mul`
`fromRows_neg` 📖	mathematical	—	`Matrix` `neg` `fromRows`	—	`ext`
`fromRows_toRows` 📖	mathematical	—	`fromRows` `toRows₁` `toRows₂`	—	`ext`
`fromRows_zero` 📖	mathematical	—	`fromRows` `Matrix` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`ext`
`mul_fromCols` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `fromCols`	—	`ext` `Finset.sum_congr`
`sumElim_vecMul_fromRows` 📖	mathematical	—	`vecMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instFintypeSum` `fromRows` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	`Finset.sum_congr` `Fintype.sum_sum_type`
`toCols₁_apply` 📖	mathematical	—	`toCols₁`	—	—
`toCols₁_fromCols` 📖	mathematical	—	`toCols₁` `fromCols`	—	—
`toCols₂_apply` 📖	mathematical	—	`toCols₂`	—	—
`toCols₂_fromCols` 📖	mathematical	—	`toCols₂` `fromCols`	—	—
`toRows₁_apply` 📖	mathematical	—	`toRows₁`	—	—
`toRows₁_fromRows` 📖	mathematical	—	`toRows₁` `fromRows`	—	—
`toRows₂_apply` 📖	mathematical	—	`toRows₂`	—	—
`toRows₂_fromRows` 📖	mathematical	—	`toRows₂` `fromRows`	—	—
`transpose_fromCols` 📖	mathematical	—	`transpose` `fromCols` `fromRows`	—	`ext`
`transpose_fromRows` 📖	mathematical	—	`transpose` `fromRows` `fromCols`	—	`ext`
`vecMul_fromCols` 📖	mathematical	—	`vecMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `fromCols`	—	—
`vecMul_fromRows` 📖	mathematical	—	`vecMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instFintypeSum` `fromRows` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	—

---

← Back to Index