Misc

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

Statistics

Metric	Count
Definitions	0
Theorems det_eq_sum_column_mul_submatrix_succAbove_succAbove_det, det_eq_sum_row_mul_submatrix_succAbove_succAbove_det, submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det, submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det'	4
Total	4

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det_eq_sum_column_mul_submatrix_succAbove_succAbove_det 📖	mathematical	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.univ Fin.fintype MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	det Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne submatrix Fin.succAbove	—	one_smul det_updateRow_sum det_succ_row Finset.sum_congr updateRow.congr_simp updateRow_apply Finset.sum_apply det.congr_simp submatrix_updateRow_succAbove Fintype.sum_eq_add_sum_subtype_ne Subtype.prop MulZeroClass.mul_zero MulZeroClass.zero_mul Finset.sum_const_zero add_zero
det_eq_sum_row_mul_submatrix_succAbove_succAbove_det 📖	mathematical	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.univ Fin.fintype MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	det Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne submatrix Fin.succAbove	—	det_transpose det_eq_sum_column_mul_submatrix_succAbove_succAbove_det Finset.sum_congr transpose_submatrix transpose_transpose add_comm
submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det 📖	mathematical	Finset.sum Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.univ Fin.fintype Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	det submatrix Fin.succAbove Units Int.instMonoid Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Int.negOnePow	—	Nat.cast_zero Int.negOnePow_zero one_smul Nat.cast_add Nat.cast_one Int.negOnePow_succ Units.neg_smul neg_eq_iff_eq_neg neg_one_smul det_updateRow_sum ext updateRow.congr_simp Finset.sum_congr updateRow_apply Finset.sum_neg_distrib Finset.sum_apply Fin.succAbove_castSucc_self neg_eq_iff_add_eq_zero add_comm Pi.add_apply Fin.sum_univ_succAbove ne_iff_lt_or_gt Fin.succAbove_castSucc_of_lt Fin.succAbove_of_succ_le LT.lt.le Fin.succAbove_succ_of_lt Fin.succAbove_castSucc_of_le smul_smul Int.negOnePow_add sub_add_cancel
submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det' 📖	mathematical	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.univ Fin.fintype MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	det submatrix Fin.succAbove Units Int.instMonoid Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Int.negOnePow	—	det_transpose transpose_submatrix submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det Finset.sum_apply Finset.sum_congr transpose_transpose

---

← Back to Index