TotallyUnimodular

📁 Source: Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean

Statistics

Metric	Count
Definitions IsTotallyUnimodular	1
Theorems apply, fromCols_one, fromRows_one, fromRows_unitlike, one_fromCols, one_fromRows, reindex, submatrix, transpose, emptyCols_isTotallyUnimodular, emptyRows_isTotallyUnimodular, fromCols_one_isTotallyUnimodular_iff, fromCols_replicateCol0_isTotallyUnimodular_iff, fromRows_isTotallyUnimodular_iff_rows, fromRows_one_isTotallyUnimodular_iff, fromRows_replicateRow0_isTotallyUnimodular_iff, isTotallyUnimodular_iff, isTotallyUnimodular_iff_fintype, one_fromCols_isTotallyUnimodular_iff, one_fromRows_isTotallyUnimodular_iff, reindex_isTotallyUnimodular, transpose_isTotallyUnimodular_iff	22
Total	23

Matrix

Definitions

Name	Category	Theorems
IsTotallyUnimodular 📖	MathDef	13 math math: isTotallyUnimodular_iff, emptyCols_isTotallyUnimodular, isTotallyUnimodular_iff_fintype, one_fromCols_isTotallyUnimodular_iff, one_fromRows_isTotallyUnimodular_iff, fromCols_replicateCol0_isTotallyUnimodular_iff, fromRows_isTotallyUnimodular_iff_rows, reindex_isTotallyUnimodular, transpose_isTotallyUnimodular_iff, fromRows_one_isTotallyUnimodular_iff, fromRows_replicateRow0_isTotallyUnimodular_iff, emptyRows_isTotallyUnimodular, fromCols_one_isTotallyUnimodular_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
emptyCols_isTotallyUnimodular 📖	mathematical	—	IsTotallyUnimodular	—	IsTotallyUnimodular.transpose emptyRows_isTotallyUnimodular
emptyRows_isTotallyUnimodular 📖	mathematical	—	IsTotallyUnimodular	—	submatrix_empty det_fin_zero SignType.coe_one IsEmpty.false
fromCols_one_isTotallyUnimodular_iff 📖	mathematical	—	IsTotallyUnimodular fromCols Matrix one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	transpose_isTotallyUnimodular_iff transpose_fromCols transpose_one fromRows_one_isTotallyUnimodular_iff
fromCols_replicateCol0_isTotallyUnimodular_iff 📖	mathematical	—	IsTotallyUnimodular fromCols replicateCol Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	transpose_isTotallyUnimodular_iff transpose_fromCols transpose_replicateCol fromRows_replicateRow0_isTotallyUnimodular_iff
fromRows_isTotallyUnimodular_iff_rows 📖	mathematical	Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SignType.cast AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	IsTotallyUnimodular fromRows	—	IsTotallyUnimodular.submatrix IsTotallyUnimodular.fromRows_unitlike
fromRows_one_isTotallyUnimodular_iff 📖	mathematical	—	IsTotallyUnimodular fromRows Matrix one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	fromRows_isTotallyUnimodular_iff_rows Pi.single_apply
fromRows_replicateRow0_isTotallyUnimodular_iff 📖	mathematical	—	IsTotallyUnimodular fromRows replicateRow Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	fromRows_isTotallyUnimodular_iff_rows Pi.single_apply
isTotallyUnimodular_iff 📖	mathematical	—	IsTotallyUnimodular Set Set.instMembership Set.range SignType SignType.cast MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup det Fin.fintype submatrix	—	SignType.coe_zero det_transpose transpose_submatrix det_zero_of_column_eq
isTotallyUnimodular_iff_fintype 📖	mathematical	—	IsTotallyUnimodular Set Set.instMembership Set.range SignType SignType.cast MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup det submatrix	—	isTotallyUnimodular_iff det_submatrix_equiv_self submatrix_submatrix
one_fromCols_isTotallyUnimodular_iff 📖	mathematical	—	IsTotallyUnimodular fromCols Matrix one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	transpose_isTotallyUnimodular_iff transpose_fromCols transpose_one one_fromRows_isTotallyUnimodular_iff
one_fromRows_isTotallyUnimodular_iff 📖	mathematical	—	IsTotallyUnimodular fromRows Matrix one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	ext reindex_isTotallyUnimodular fromRows_one_isTotallyUnimodular_iff
reindex_isTotallyUnimodular 📖	mathematical	—	IsTotallyUnimodular DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike reindex	—	submatrix_submatrix Equiv.symm_comp_self submatrix_id_id IsTotallyUnimodular.reindex
transpose_isTotallyUnimodular_iff 📖	mathematical	—	IsTotallyUnimodular transpose	—	IsTotallyUnimodular.transpose

Matrix.IsTotallyUnimodular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply 📖	mathematical	Matrix.IsTotallyUnimodular	Set Set.instMembership Set.range SignType SignType.cast MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	Matrix.det_unique Matrix.isTotallyUnimodular_iff
fromCols_one 📖	mathematical	Matrix.IsTotallyUnimodular	Matrix.fromCols Matrix Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Matrix.fromCols_one_isTotallyUnimodular_iff
fromRows_one 📖	mathematical	Matrix.IsTotallyUnimodular	Matrix.fromRows Matrix Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Matrix.fromRows_one_isTotallyUnimodular_iff
fromRows_unitlike 📖	mathematical	Matrix.IsTotallyUnimodular Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SignType.cast AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	Matrix.fromRows	—	Matrix.det.congr_simp Matrix.submatrix_empty Matrix.det_fin_zero Matrix.det_succ_row Pi.single_eq_same Fintype.sum_eq_single Pi.single_eq_of_ne MulZeroClass.mul_zero Matrix.submatrix_submatrix MulZeroClass.zero_mul MulMemClass.mul_mem SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass MonoidHom.instMonoidHomClass pow_mem SignType.coe_neg Set.mem_range_self Fin.succAbove_right_injective Finset.sum_congr Finset.sum_const_zero Matrix.isTotallyUnimodular_iff
one_fromCols 📖	mathematical	Matrix.IsTotallyUnimodular	Matrix.fromCols Matrix Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Matrix.one_fromCols_isTotallyUnimodular_iff
one_fromRows 📖	mathematical	Matrix.IsTotallyUnimodular	Matrix.fromRows Matrix Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Matrix.one_fromRows_isTotallyUnimodular_iff
reindex 📖	mathematical	Matrix.IsTotallyUnimodular	DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike Matrix.reindex	—	submatrix
submatrix 📖	mathematical	Matrix.IsTotallyUnimodular	Matrix.submatrix	—	Matrix.det.congr_simp Matrix.submatrix_submatrix
transpose 📖	mathematical	Matrix.IsTotallyUnimodular	Matrix.transpose	—	Matrix.det.congr_simp Matrix.det_transpose

---

← Back to Index