Transvection

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

Statistics

Metric	Count
Definitions listTransvecCol, listTransvecRow, TransvectionStruct, c, i, inv, j, reindexEquiv, sumInl, toMatrix, transvection	11
Theorems exists_isTwoBlockDiagonal_list_transvec_mul_mul_list_transvec, exists_isTwoBlockDiagonal_of_ne_zero, exists_list_transvec_mul_diagonal_mul_list_transvec, exists_list_transvec_mul_mul_list_transvec_eq_diagonal, exists_list_transvec_mul_mul_list_transvec_eq_diagonal_aux, exists_list_transvec_mul_mul_list_transvec_eq_diagonal_induction, isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRow, length_listTransvecCol, length_listTransvecRow, listTransvecCol_getElem, listTransvecCol_mul_last_col, listTransvecCol_mul_last_row, listTransvecCol_mul_last_row_drop, listTransvecCol_mul_mul_listTransvecRow_last_col, listTransvecCol_mul_mul_listTransvecRow_last_row, listTransvecRow_getElem, mul_listTransvecRow_last_col, mul_listTransvecRow_last_col_take, mul_listTransvecRow_last_row, reindex_exists_list_transvec_mul_mul_list_transvec_eq_diagonal, det, det_toMatrix_prod, hij, inv_c, inv_i, inv_j, inv_mul, mul_inv, mul_sumInl_toMatrix_prod, prod_mul_reverse_inv_prod, reverse_inv_prod_mul_prod, sumInl_toMatrix_prod_mul, toMatrix_mk, toMatrix_reindexEquiv, toMatrix_reindexEquiv_prod, toMatrix_sumInl, det_transvection_of_ne, diagonal_transvection_induction, diagonal_transvection_induction_of_det_ne_zero, instNonemptyTransvectionStructOfNontrivial, mem_range_scalar_iff_commute_transvectionStruct, mem_range_scalar_of_commute_transvectionStruct, mul_transvection_apply_of_ne, mul_transvection_apply_same, transvection_mul_apply_of_ne, transvection_mul_apply_same, transvection_mul_transvection_same, transvection_zero, updateRow_eq_transvection	49
Total	60

Matrix

Definitions

Name	Category	Theorems
TransvectionStruct 📖	CompData	12 math math: Pivot.exists_isTwoBlockDiagonal_list_transvec_mul_mul_list_transvec, TransvectionStruct.det_toMatrix_prod, TransvectionStruct.toMatrix_reindexEquiv_prod, Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_aux, TransvectionStruct.prod_mul_reverse_inv_prod, TransvectionStruct.mul_sumInl_toMatrix_prod, Pivot.exists_isTwoBlockDiagonal_of_ne_zero, Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal, Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec, TransvectionStruct.sumInl_toMatrix_prod_mul, TransvectionStruct.reverse_inv_prod_mul_prod, instNonemptyTransvectionStructOfNontrivial
transvection 📖	CompOp	13 math math: blockTriangular_transvection', updateRow_eq_transvection, transvection_mul_transvection_same, Pivot.listTransvecCol_getElem, transvection_zero, transvection_mul_apply_same, det_transvection_of_ne, TransvectionStruct.toMatrix_mk, mul_transvection_apply_of_ne, blockTriangular_transvection, transvection_mul_apply_of_ne, Pivot.listTransvecRow_getElem, mul_transvection_apply_same

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det_transvection_of_ne 📖	mathematical	—	det transvection AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	updateRow_eq_transvection Finite.of_fintype det_updateRow_add_smul_self det_one
diagonal_transvection_induction 📖	—	diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing TransvectionStruct.toMatrix Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid	—	—	Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec det_diagonal det.congr_simp det_mul TransvectionStruct.det_toMatrix_prod one_mul mul_one one_mul mul_assoc
diagonal_transvection_induction_of_det_ne_zero 📖	—	diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing TransvectionStruct.toMatrix Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid	—	—	diagonal_transvection_induction TransvectionStruct.det NeZero.one DivisionRing.toNontrivial det_mul IsDomain.to_noZeroDivisors Field.isDomain
instNonemptyTransvectionStructOfNontrivial 📖	mathematical	—	TransvectionStruct	—	exists_pair_ne
mem_range_scalar_iff_commute_transvectionStruct 📖	mathematical	—	Matrix Set Set.instMembership Set.range DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring nonAssocSemiring RingHom.instFunLike scalar Commute instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid TransvectionStruct.toMatrix	—	Commute.add_left Commute.one_left smul_single smul_eq_mul mul_one Commute.smul_left Algebra.to_smulCommClass IsScalarTower.right mem_range_scalar_iff_commute_single TransvectionStruct.hij mem_range_scalar_of_commute_transvectionStruct
mem_range_scalar_of_commute_transvectionStruct 📖	mathematical	Commute Matrix instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid TransvectionStruct.toMatrix	Set Set.instMembership Set.range DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring nonAssocSemiring RingHom.instFunLike scalar	—	mem_range_scalar_of_commute_single add_mul Distrib.rightDistribClass one_mul mul_add Distrib.leftDistribClass mul_one AddLeftCancelSemigroup.toIsLeftCancelAdd Commute.eq
mul_transvection_apply_of_ne 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid transvection	—	mul_add mul_one mul_single_apply_of_ne add_zero
mul_transvection_apply_same 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid transvection Distrib.toAdd	—	mul_add mul_one mul_single_apply_same mul_comm
transvection_mul_apply_of_ne 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid transvection	—	add_mul one_mul single_mul_apply_of_ne add_zero
transvection_mul_apply_same 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid transvection Distrib.toAdd	—	add_mul one_mul single_mul_apply_same
transvection_mul_transvection_same 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid transvection Distrib.toAdd	—	mul_add mul_one add_mul one_mul single_mul_single_of_ne add_zero add_assoc single_add
transvection_zero 📖	mathematical	—	transvection MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Matrix one AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	single_zero add_zero
updateRow_eq_transvection 📖	mathematical	—	updateRow Matrix one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id transvection	—	nonempty_fintype ext updateRow.congr_simp updateRow_self mul_one single_apply_same MulZeroClass.mul_zero add_zero single_apply_of_ne updateRow_ne

Matrix.Pivot

Definitions

Name	Category	Theorems
listTransvecCol 📖	CompOp	7 math math: listTransvecCol_mul_mul_listTransvecRow_last_col, listTransvecCol_mul_last_col, listTransvecCol_mul_last_row_drop, listTransvecCol_mul_mul_listTransvecRow_last_row, isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRow, listTransvecCol_mul_last_row, length_listTransvecCol
listTransvecRow 📖	CompOp	7 math math: listTransvecCol_mul_mul_listTransvecRow_last_col, length_listTransvecRow, mul_listTransvecRow_last_col, mul_listTransvecRow_last_row, listTransvecCol_mul_mul_listTransvecRow_last_row, isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRow, mul_listTransvecRow_last_col_take

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_isTwoBlockDiagonal_list_transvec_mul_mul_list_transvec 📖	mathematical	—	Matrix.IsTwoBlockDiagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid instFintypeSum Fin.fintype PUnit.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.instMulOfFintypeOfAddCommMonoid Matrix.one AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Matrix.TransvectionStruct Matrix.TransvectionStruct.toMatrix	—	one_mul mul_one Mathlib.Tactic.Contrapose.contrapose₂ Matrix.transvection_mul_apply_same zero_add exists_isTwoBlockDiagonal_of_ne_zero Semigroup.to_isLawfulIdentity Semigroup.to_isAssociative Matrix.mul_one Matrix.mul_assoc Matrix.mul_transvection_apply_same
exists_isTwoBlockDiagonal_of_ne_zero 📖	mathematical	—	Matrix.IsTwoBlockDiagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid instFintypeSum Fin.fintype PUnit.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.instMulOfFintypeOfAddCommMonoid Matrix.one AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Matrix.TransvectionStruct Matrix.TransvectionStruct.toMatrix	—	List.map_ofFn isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRow
exists_list_transvec_mul_diagonal_mul_list_transvec 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.instMulOfFintypeOfAddCommMonoid Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Matrix.TransvectionStruct Matrix.TransvectionStruct.toMatrix Matrix.diagonal	—	exists_list_transvec_mul_mul_list_transvec_eq_diagonal Matrix.TransvectionStruct.reverse_inv_prod_mul_prod Matrix.TransvectionStruct.prod_mul_reverse_inv_prod Matrix.one_mul Matrix.mul_one Matrix.mul_assoc
exists_list_transvec_mul_mul_list_transvec_eq_diagonal 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.instMulOfFintypeOfAddCommMonoid Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Matrix.TransvectionStruct Matrix.TransvectionStruct.toMatrix Matrix.diagonal	—	Fintype.card_fin reindex_exists_list_transvec_mul_mul_list_transvec_eq_diagonal exists_list_transvec_mul_mul_list_transvec_eq_diagonal_aux
exists_list_transvec_mul_mul_list_transvec_eq_diagonal_aux 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.instMulOfFintypeOfAddCommMonoid Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Matrix.TransvectionStruct Matrix.TransvectionStruct.toMatrix Matrix.diagonal	—	Matrix.ext Fintype.card_eq_zero_iff Fintype.card_sum Fintype.card_fin Fintype.card_unique reindex_exists_list_transvec_mul_mul_list_transvec_eq_diagonal exists_list_transvec_mul_mul_list_transvec_eq_diagonal_induction
exists_list_transvec_mul_mul_list_transvec_eq_diagonal_induction 📖	mathematical	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Fin.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.instMulOfFintypeOfAddCommMonoid Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Matrix.TransvectionStruct Matrix.TransvectionStruct.toMatrix Matrix.diagonal	instFintypeSum PUnit.fintype	—	exists_isTwoBlockDiagonal_list_transvec_mul_mul_list_transvec Matrix.fromBlocks_toBlocks Matrix.TransvectionStruct.sumInl_toMatrix_prod_mul Matrix.TransvectionStruct.mul_sumInl_toMatrix_prod Matrix.fromBlocks_diagonal Semigroup.to_isLawfulIdentity Semigroup.to_isAssociative Matrix.mul_assoc
isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRow 📖	mathematical	—	Matrix.IsTwoBlockDiagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid instFintypeSum Fin.fintype PUnit.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.instMulOfFintypeOfAddCommMonoid Matrix.one AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing listTransvecCol listTransvecRow	—	Matrix.ext listTransvecCol_mul_mul_listTransvecRow_last_row listTransvecCol_mul_mul_listTransvecRow_last_col
length_listTransvecCol 📖	mathematical	—	Matrix listTransvecCol	—	—
length_listTransvecRow 📖	mathematical	—	Matrix listTransvecRow	—	—
listTransvecCol_getElem 📖	mathematical	Matrix listTransvecCol	Matrix.transvection Field.toCommRing length_listTransvecCol DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing	—	length_listTransvecCol
listTransvecCol_mul_last_col 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid instFintypeSum Fin.fintype PUnit.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.instMulOfFintypeOfAddCommMonoid Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing listTransvecCol	—	Matrix.mul_assoc Matrix.transvection_mul_apply_same IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le listTransvecCol_mul_last_row_drop Nat.instCanonicallyOrderedAdd Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one neg_div neg_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero mul_neg Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one one_ne_zero NeZero.one GroupWithZero.toNontrivial add_neg_cancel MulZeroClass.mul_zero Matrix.transvection_mul_apply_of_ne le_or_gt LE.le.trans length_listTransvecCol Matrix.one_mul zero_le
listTransvecCol_mul_last_row 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid instFintypeSum Fin.fintype PUnit.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.instMulOfFintypeOfAddCommMonoid Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing listTransvecCol	—	listTransvecCol_mul_last_row_drop zero_le Nat.instCanonicallyOrderedAdd
listTransvecCol_mul_last_row_drop 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid instFintypeSum Fin.fintype PUnit.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.instMulOfFintypeOfAddCommMonoid Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing listTransvecCol	—	Matrix.mul_assoc Matrix.transvection_mul_apply_of_ne length_listTransvecCol Matrix.one_mul
listTransvecCol_mul_mul_listTransvecRow_last_col 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid instFintypeSum Fin.fintype PUnit.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.instMulOfFintypeOfAddCommMonoid Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing listTransvecCol listTransvecRow	—	listTransvecCol_mul_last_row mul_listTransvecRow_last_row
listTransvecCol_mul_mul_listTransvecRow_last_row 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid instFintypeSum Fin.fintype PUnit.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.instMulOfFintypeOfAddCommMonoid Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing listTransvecCol listTransvecRow	—	mul_listTransvecRow_last_col Matrix.mul_assoc listTransvecCol_mul_last_col
listTransvecRow_getElem 📖	mathematical	Matrix listTransvecRow	Matrix.transvection Field.toCommRing length_listTransvecRow DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing	—	length_listTransvecRow
mul_listTransvecRow_last_col 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid instFintypeSum Fin.fintype PUnit.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.instMulOfFintypeOfAddCommMonoid Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing listTransvecRow	—	mul_listTransvecRow_last_col_take le_rfl
mul_listTransvecRow_last_col_take 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid instFintypeSum Fin.fintype PUnit.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.instMulOfFintypeOfAddCommMonoid Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing listTransvecRow	—	Matrix.mul_one Semigroup.to_isLawfulIdentity Semigroup.to_isAssociative Matrix.mul_transvection_apply_of_ne LT.lt.le
mul_listTransvecRow_last_row 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid instFintypeSum Fin.fintype PUnit.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.instMulOfFintypeOfAddCommMonoid Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing listTransvecRow	—	Matrix.mul_one Semigroup.to_isLawfulIdentity Semigroup.to_isAssociative Matrix.mul_transvection_apply_same LT.lt.le Eq.le mul_listTransvecRow_last_col_take Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one neg_div neg_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero mul_neg Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Matrix.mul_transvection_apply_of_ne le_or_gt LE.le.trans le_rfl
reindex_exists_list_transvec_mul_mul_list_transvec_eq_diagonal 📖	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.instMulOfFintypeOfAddCommMonoid Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Matrix.TransvectionStruct Matrix.TransvectionStruct.toMatrix DFunLike.coe AlgEquiv Semifield.toCommSemiring Field.toSemifield Matrix.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Matrix.instAlgebra Algebra.id AlgEquiv.instFunLike Matrix.reindexAlgEquiv Matrix.diagonal	—	—	Matrix.submatrix_submatrix Equiv.symm_comp_self Matrix.submatrix_id_id Matrix.TransvectionStruct.toMatrix_reindexEquiv_prod Matrix.reindexAlgEquiv_apply Matrix.submatrix_diagonal_equiv

Matrix.TransvectionStruct

Definitions

Name	Category	Theorems
c 📖	CompOp	1 math math: inv_c
i 📖	CompOp	1 math math: inv_i
inv 📖	CompOp	7 math math: inv_c, inv_j, inv_mul, prod_mul_reverse_inv_prod, inv_i, reverse_inv_prod_mul_prod, mul_inv
j 📖	CompOp	1 math math: inv_j
reindexEquiv 📖	CompOp	2 math math: toMatrix_reindexEquiv_prod, toMatrix_reindexEquiv
sumInl 📖	CompOp	3 math math: mul_sumInl_toMatrix_prod, sumInl_toMatrix_prod_mul, toMatrix_sumInl
toMatrix 📖	CompOp	19 math math: Matrix.mem_range_scalar_iff_commute_transvectionStruct, det, Matrix.Pivot.exists_isTwoBlockDiagonal_list_transvec_mul_mul_list_transvec, det_toMatrix_prod, inv_mul, toMatrix_reindexEquiv_prod, Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_aux, toMatrix_reindexEquiv, prod_mul_reverse_inv_prod, mul_sumInl_toMatrix_prod, toMatrix_mk, Matrix.Pivot.exists_isTwoBlockDiagonal_of_ne_zero, Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal, Matrix.Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec, sumInl_toMatrix_prod_mul, reverse_inv_prod_mul_prod, toMatrix_sumInl, Real.volume_preserving_transvectionStruct, mul_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det 📖	mathematical	—	Matrix.det toMatrix AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Matrix.det_transvection_of_ne hij
det_toMatrix_prod 📖	mathematical	—	Matrix.det Matrix Matrix.instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.TransvectionStruct toMatrix	—	Matrix.det_one Matrix.det_mul det mul_one
hij 📖	—	—	—	—	—
inv_c 📖	mathematical	—	c inv NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	—
inv_i 📖	mathematical	—	i inv	—	—
inv_j 📖	mathematical	—	j inv	—	—
inv_mul 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid toMatrix inv Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Matrix.transvection_mul_transvection_same neg_add_cancel Matrix.transvection_zero
mul_inv 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid toMatrix inv Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Matrix.transvection_mul_transvection_same add_neg_cancel Matrix.transvection_zero
mul_sumInl_toMatrix_prod 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid instFintypeSum Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.fromBlocks Matrix.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Matrix.instMulOfFintypeOfAddCommMonoid Matrix.one AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.TransvectionStruct toMatrix sumInl	—	mul_one toMatrix_sumInl Matrix.fromBlocks_multiply Matrix.mul_zero add_zero Matrix.mul_one Matrix.zero_mul zero_add
prod_mul_reverse_inv_prod 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.instMulOfFintypeOfAddCommMonoid Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.TransvectionStruct toMatrix inv	—	mul_one Matrix.mul_one mul_inv Semigroup.to_isLawfulIdentity Semigroup.to_isAssociative Matrix.mul_assoc
reverse_inv_prod_mul_prod 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.instMulOfFintypeOfAddCommMonoid Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.TransvectionStruct toMatrix inv	—	mul_one inv_mul Semigroup.to_isLawfulIdentity Semigroup.to_isAssociative Matrix.mul_assoc
sumInl_toMatrix_prod_mul 📖	mathematical	—	Matrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid instFintypeSum Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.instMulOfFintypeOfAddCommMonoid Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.TransvectionStruct toMatrix sumInl Matrix.fromBlocks Matrix.zero	—	one_mul toMatrix_sumInl Matrix.mul_assoc Matrix.fromBlocks_multiply Matrix.mul_zero add_zero Matrix.zero_mul zero_add
toMatrix_mk 📖	mathematical	—	toMatrix Matrix.transvection	—	—
toMatrix_reindexEquiv 📖	mathematical	—	toMatrix reindexEquiv DFunLike.coe AlgEquiv Matrix CommRing.toCommSemiring Matrix.semiring CommSemiring.toSemiring Matrix.instAlgebra Algebra.id AlgEquiv.instFunLike Matrix.reindexAlgEquiv	—	Matrix.ext Matrix.one_apply_eq Equiv.apply_eq_iff_eq_symm_apply Matrix.one_apply_ne zero_add Equiv.apply_symm_apply add_zero
toMatrix_reindexEquiv_prod 📖	mathematical	—	Matrix Matrix.instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.TransvectionStruct toMatrix reindexEquiv DFunLike.coe AlgEquiv CommRing.toCommSemiring Matrix.semiring CommSemiring.toSemiring Matrix.instAlgebra Algebra.id AlgEquiv.instFunLike Matrix.reindexAlgEquiv	—	Matrix.submatrix_one_equiv toMatrix_reindexEquiv Matrix.reindexAlgEquiv_mul
toMatrix_sumInl 📖	mathematical	—	toMatrix sumInl Matrix.fromBlocks Matrix Matrix.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Matrix.one AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Matrix.ext toMatrix.congr_simp Matrix.one_apply_eq Matrix.one_apply_ne zero_add Matrix.single_apply_of_ne add_zero

---

← Back to Index