NonsingularInverse

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

Statistics

Metric	Count
Definitions detInvertibleOfInvertible, detInvertibleOfLeftInverse, detInvertibleOfRightInverse, diagonalInvertible, diagonalInvertibleEquivInvertible, instInvOneClass, instInvertibleInv, inv, invertibleEquivDetInvertible, invertibleOfDetInvertible, invertibleOfDiagonalInvertible, invertibleOfIsUnitDet, invertibleOfSubmatrixEquivInvertible, nonsingInvUnit, submatrixEquivInvertible, submatrixEquivInvertibleEquivInvertible, unitOfDetInvertible	17
Theorems inv, add_mul_mul_inv_eq_sub, add_mul_mul_inv_eq_sub', coe_units_inv, conjTranspose_nonsing_inv, det_conj, det_conj', det_invOf, det_ne_zero_of_left_inverse, det_ne_zero_of_right_inverse, det_nonsing_inv, det_nonsing_inv_mul_det, det_smul_inv_mulVec_eq_cramer, det_smul_inv_vecMul_eq_cramer_transpose, diagonalInvertibleEquivInvertible_apply, diagonalInvertibleEquivInvertible_symm_apply, invOf_diagonal_eq, invOf_eq, invOf_eq_nonsing_inv, invOf_submatrix_equiv_eq, inv_add_inv, inv_adjugate, inv_def, inv_diagonal, inv_eq_left_inv, inv_eq_right_inv, inv_inj, inv_inv_inv, inv_inv_of_invertible, inv_kronecker, inv_mulVec_eq_vec, inv_mul_cancel_left_of_invertible, inv_mul_cancel_right_of_invertible, inv_mul_eq_iff_eq_mul_of_invertible, inv_mul_of_invertible, inv_reindex, inv_smul, inv_smul', inv_sub_inv, inv_submatrix_equiv, inv_subsingleton, inv_zero, invertibleEquivDetInvertible_apply, invertibleEquivDetInvertible_symm_apply, isUnit_det_of_invertible, isUnit_det_of_left_inverse, isUnit_det_of_right_inverse, isUnit_det_transpose, isUnit_diagonal, isUnit_iff_isUnit_det, isUnit_nonsing_inv_det, isUnit_nonsing_inv_det_iff, isUnit_nonsing_inv_iff, isUnit_submatrix_equiv, isUnits_det_units, left_inv_eq_left_inv, linearIndependent_cols_iff_isUnit, linearIndependent_cols_of_invertible, linearIndependent_rows_iff_isUnit, linearIndependent_rows_of_invertible, list_prod_inv_reverse, mulVec_injective_iff_isUnit, mulVec_injective_of_invertible, mulVec_surjective_iff_exists_right_inverse, mulVec_surjective_iff_isUnit, mulVec_surjective_of_invertible, mul_inv_cancel_left_of_invertible, mul_inv_cancel_right_of_invertible, mul_inv_eq_iff_eq_mul_of_invertible, mul_inv_of_invertible, mul_inv_rev, mul_left_inj_of_invertible, mul_left_injective_of_inv, mul_left_injective_of_invertible, mul_nonsing_inv, mul_nonsing_inv_cancel_left, mul_nonsing_inv_cancel_right, mul_right_inj_of_invertible, mul_right_injective_of_inv, mul_right_injective_of_invertible, nonsing_inv_apply, nonsing_inv_apply_not_isUnit, nonsing_inv_cancel_or_zero, nonsing_inv_eq_ringInverse, nonsing_inv_mul, nonsing_inv_mul_cancel_left, nonsing_inv_mul_cancel_right, nonsing_inv_nonsing_inv, right_inv_eq_left_inv, right_inv_eq_right_inv, submatrixEquivInvertibleEquivInvertible_apply, submatrixEquivInvertibleEquivInvertible_symm_apply, trace_conj, trace_conj', transpose_nonsing_inv, unitOfDetInvertible_eq_nonsingInvUnit, vecMul_injective_iff_isUnit, vecMul_injective_of_invertible, vecMul_surjective_iff_exists_left_inverse, vecMul_surjective_iff_isUnit, vecMul_surjective_of_invertible	101
Total	118

Matrix

Definitions

Name	Category	Theorems
detInvertibleOfInvertible 📖	CompOp	1 math math: invertibleEquivDetInvertible_apply
detInvertibleOfLeftInverse 📖	CompOp	—
detInvertibleOfRightInverse 📖	CompOp	—
diagonalInvertible 📖	CompOp	1 math math: diagonalInvertibleEquivInvertible_symm_apply
diagonalInvertibleEquivInvertible 📖	CompOp	2 math math: diagonalInvertibleEquivInvertible_symm_apply, diagonalInvertibleEquivInvertible_apply
instInvOneClass 📖	CompOp	—
instInvertibleInv 📖	CompOp	—
inv 📖	CompOp	115 math math: discr_conj, list_prod_inv_reverse, inv_mul_eq_iff_eq_mul_of_invertible, det_smul_inv_mulVec_eq_cramer, det_add_replicateCol_mul_replicateRow, lieConj_apply, LieAlgebra.Orthogonal.soIndefiniteEquiv_apply, IsHermitian.fromBlocks₂₂, mul_inv_eq_iff_eq_mul_of_invertible, zpow_neg_one, inv_fromBlocks_zero₁₂_of_isUnit_iff, isHyperbolic_conj_iff, exp_conj', exp_neg, isHyperbolic_conj'_iff, isElliptic_conj'_iff, PosDef.fromBlocks₁₁, mul_inv_of_invertible, coe_units_inv, det_add_mul, add_mul_mul_inv_eq_sub', add_mul_mul_inv_eq_sub, isParabolic_conj'_iff, inv_zero, mul_inv_cancel_right_of_invertible, inv_add_inv, inv_smul', inv_sub_inv, isUnit_nonsing_inv_det_iff, invOf_eq_nonsing_inv, inv_smul, inv_reindex, conjTranspose_nonsing_inv, nonsing_inv_mul, isAdjointPair_equiv', inv_def, isParabolic_conj_iff, schur_complement_eq₂₂, nonsing_inv_nonsing_inv, inv_eq_right_inv, continuousAt_matrix_inv, inv_adjugate, isElliptic_conj_iff, nonsing_inv_eq_ringInverse, lieConj_symm_apply, isHermitian_inv, nonsing_inv_apply, inv_eq_left_inv, det_conj', BlockTriangular.toBlock_inverse_mul_toBlock_eq_one, isAdjointPair_equiv, schur_complement_eq₁₁, mul_inv_cancel_left_of_invertible, det_nonsing_inv_mul_det, AffineBasis.toMatrix_inv_vecMul_toMatrix, exp_conj, PosDef.fromBlocks₂₂, IsHermitian.inv, nonsing_inv_cancel_or_zero, inv_pow', NumberField.inverse_basisMatrix_mulVec_eq_repr, GeneralLinearGroup.coe_inv, nonsing_inv_apply_not_isUnit, PosSemidef.inv_sqrt, inv_mul_cancel_right_of_invertible, discr_conj', mul_inv_rev, toBlock_inverse_eq_zero, mul_nonsing_inv_cancel_right, inv_kronecker, pow_sub', inv_mul_of_invertible, zpow_neg, det_conj, GeneralLinearGroup.coe_map_mul_map_inv, isUnit_nonsing_inv_iff, blockTriangular_inv_of_blockTriangular, nonsing_inv_mul_cancel_right, inv_zpow', disc_conj, inv_fromBlocks_zero₂₁_of_isUnit_iff, inv_submatrix_equiv, J_inv, posDef_inv_iff, transpose_nonsing_inv, mul_nonsing_inv_cancel_left, IsHermitian.fromBlocks₁₁, charpoly_inv, BlockTriangular.inv_toBlock, nonsing_inv_mul_cancel_left, IsSymm.inv, zpow_sub_one, SymplecticGroup.coe_inv', inv_zpow, pow_inv_comm', disc_conj', LinearEquiv.ofIsUnitDet_symm_apply, skewAdjointMatricesLieSubalgebraEquiv_apply, zpow_neg_natCast, PosSemidef.inv, GeneralLinearGroup.coe_map_inv_mul_map, mul_nonsing_inv, inv_mulVec_eq_vec, inv_subsingleton, inv_mul_cancel_left_of_invertible, trace_conj', inv_diagonal, SymplecticGroup.inv_eq_symplectic_inv, isUnit_nonsing_inv_det, inv_inv_inv, trace_conj, det_nonsing_inv, PosDef.inv, inv_inv_of_invertible, det_smul_inv_vecMul_eq_cramer_transpose
invertibleEquivDetInvertible 📖	CompOp	2 math math: invertibleEquivDetInvertible_apply, invertibleEquivDetInvertible_symm_apply
invertibleOfDetInvertible 📖	CompOp	1 math math: invertibleEquivDetInvertible_symm_apply
invertibleOfDiagonalInvertible 📖	CompOp	1 math math: diagonalInvertibleEquivInvertible_apply
invertibleOfIsUnitDet 📖	CompOp	—
invertibleOfSubmatrixEquivInvertible 📖	CompOp	1 math math: submatrixEquivInvertibleEquivInvertible_apply
nonsingInvUnit 📖	CompOp	1 math math: unitOfDetInvertible_eq_nonsingInvUnit
submatrixEquivInvertible 📖	CompOp	1 math math: submatrixEquivInvertibleEquivInvertible_symm_apply
submatrixEquivInvertibleEquivInvertible 📖	CompOp	2 math math: submatrixEquivInvertibleEquivInvertible_apply, submatrixEquivInvertibleEquivInvertible_symm_apply
unitOfDetInvertible 📖	CompOp	1 math math: unitOfDetInvertible_eq_nonsingInvUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_mul_mul_inv_eq_sub 📖	mathematical	IsUnit Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing inv instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toAddCommMonoid	Matrix inv add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toAddCommMonoid sub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	IsUnit.nonempty_invertible invOf_add_mul_mul
add_mul_mul_inv_eq_sub' 📖	mathematical	IsUnit Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toAddCommMonoid inv	Matrix inv add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toAddCommMonoid sub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	IsUnit.nonempty_invertible invOf_add_mul_mul'
coe_units_inv 📖	mathematical	—	Units.val Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring Units Units.instInv inv	—	invOf_eq_nonsing_inv invOf_units
conjTranspose_nonsing_inv 📖	mathematical	—	conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing StarRing.toStarAddMonoid Matrix inv	—	inv_def conjTranspose_smul StarMul.toStarModule det_conjTranspose adjugate_conjTranspose Ring.inverse_star
det_conj 📖	mathematical	IsUnit Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring	det Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid inv	—	IsUnit.unit_spec coe_units_inv det_units_conj
det_conj' 📖	mathematical	IsUnit Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring	det Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid inv	—	IsUnit.unit_spec coe_units_inv det_units_conj'
det_invOf 📖	mathematical	—	det Invertible.invOf Matrix instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Invertible.congr
det_ne_zero_of_left_inverse 📖	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—	IsUnit.ne_zero isUnit_det_of_left_inverse
det_ne_zero_of_right_inverse 📖	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—	IsUnit.ne_zero isUnit_det_of_right_inverse
det_nonsing_inv 📖	mathematical	—	det Matrix inv Ring.inverse Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	IsUnit.nonempty_invertible Ring.inverse_invertible invOf_eq_nonsing_inv det_invOf isEmpty_or_nonempty det_isEmpty Ring.inverse_one Ring.inverse_non_unit nonsing_inv_apply_not_isUnit det_zero
det_nonsing_inv_mul_det 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing det Matrix inv AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	det_mul nonsing_inv_mul det_one
det_smul_inv_mulVec_eq_cramer 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id det mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Matrix inv DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike cramer	—	cramer_eq_adjugate_mulVec nonsing_inv_apply smul_mulVec IsScalarTower.right smul_smul IsUnit.mul_val_inv one_smul
det_smul_inv_vecMul_eq_cramer_transpose 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id det vecMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Matrix inv DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Pi.Function.module Semiring.toModule LinearMap.instFunLike cramer transpose	—	transpose_transpose vecMul_transpose transpose_nonsing_inv det_transpose det_smul_inv_mulVec_eq_cramer isUnit_det_transpose
diagonalInvertibleEquivInvertible_apply 📖	mathematical	—	DFunLike.coe Equiv Invertible Matrix instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing diagonal Pi.instMul Pi.instOne EquivLike.toFunLike Equiv.instEquivLike diagonalInvertibleEquivInvertible invertibleOfDiagonalInvertible	—	—
diagonalInvertibleEquivInvertible_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Invertible Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix instMulOfFintypeOfAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass diagonal EquivLike.toFunLike Equiv.instEquivLike Equiv.symm diagonalInvertibleEquivInvertible diagonalInvertible Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring	—	—
invOf_diagonal_eq 📖	mathematical	—	Invertible.invOf Matrix instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne diagonal Pi.instMul Pi.instOne	—	Invertible.congr
invOf_eq 📖	mathematical	—	Invertible.invOf Matrix instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing smul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id det adjugate	—	Invertible.congr
invOf_eq_nonsing_inv 📖	mathematical	—	Invertible.invOf Matrix instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing inv	—	inv_def Ring.inverse_invertible invOf_eq
invOf_submatrix_equiv_eq 📖	mathematical	—	Invertible.invOf Matrix instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing submatrix DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	Invertible.congr
inv_add_inv 📖	mathematical	IsUnit Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring	Matrix add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing inv instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toAddCommMonoid	—	nonsing_inv_eq_ringInverse Ring.inverse_add_inverse
inv_adjugate 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	Matrix inv adjugate Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instSMul smul Algebra.toSMul Algebra.id Units.instInv IsUnit.unit det	—	inv_eq_left_inv smul_mul Units.instIsScalarTower IsScalarTower.right mul_adjugate Units.smul_def smul_smul IsUnit.val_inv_mul one_smul
inv_def 📖	mathematical	—	Matrix inv smul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Ring.inverse Semiring.toMonoidWithZero det adjugate	—	—
inv_diagonal 📖	mathematical	—	Matrix inv diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ring.inverse Pi.monoidWithZero Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	nonsing_inv_eq_ringInverse isUnit_diagonal IsUnit.nonempty_invertible Ring.inverse_invertible invOf_diagonal_eq Iff.not Ring.inverse_non_unit Pi.zero_def diagonal_zero
inv_eq_left_inv 📖	mathematical	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	Matrix inv	—	instIsDedekindFiniteMonoidOfIsStablyFiniteRing instIsStablyFiniteRingOfCommSemiring invOf_eq_left_inv invOf_eq_nonsing_inv
inv_eq_right_inv 📖	mathematical	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	Matrix inv	—	inv_eq_left_inv mul_eq_one_comm instIsDedekindFiniteMonoidOfIsStablyFiniteRing instIsStablyFiniteRingOfCommSemiring
inv_inj 📖	—	Matrix inv IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	—	—	left_inv_eq_left_inv mul_nonsing_inv isUnit_nonsing_inv_det_iff
inv_inv_inv 📖	mathematical	—	Matrix inv	—	nonsing_inv_nonsing_inv nonsing_inv_apply_not_isUnit inv_zero
inv_inv_of_invertible 📖	mathematical	—	Matrix inv	—	invOf_invOf
inv_kronecker 📖	mathematical	—	Matrix inv instFintypeProd kroneckerMap Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	inv_eq_right_inv mul_kronecker_mul one_kronecker_one mul_nonsing_inv isEmpty_or_nonempty subsingleton_of_empty_right Prod.isEmpty_left isUnit_pow_iff Fintype.card_ne_zero isUnit_of_mul_isUnit_right instIsDedekindFiniteMonoid det_kronecker nonsing_inv_apply_not_isUnit kronecker_zero Prod.isEmpty_right isUnit_of_mul_isUnit_left zero_kronecker
inv_mulVec_eq_vec 📖	mathematical	mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Matrix inv	—	mulVec_mulVec inv_mul_of_invertible one_mulVec
inv_mul_cancel_left_of_invertible 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid inv	—	nonsing_inv_mul_cancel_left isUnit_det_of_invertible
inv_mul_cancel_right_of_invertible 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid inv	—	nonsing_inv_mul_cancel_right isUnit_det_of_invertible
inv_mul_eq_iff_eq_mul_of_invertible 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid inv	—	mul_inv_cancel_left_of_invertible inv_mul_cancel_left_of_invertible
inv_mul_of_invertible 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid inv one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	nonsing_inv_mul isUnit_det_of_invertible
inv_reindex 📖	mathematical	—	Matrix inv DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike reindex	—	inv_submatrix_equiv
inv_smul 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	Matrix inv smul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Invertible.invOf Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	inv_eq_left_inv Algebra.mul_smul_comm Algebra.smul_mul_assoc nonsing_inv_mul smul_smul mul_invOf_self' one_smul
inv_smul' 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	Matrix inv Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instSMul smul Algebra.toSMul Algebra.id Units.instInv	—	inv_eq_left_inv mul_smul Units.smulCommClass_left Algebra.to_smulCommClass smul_mul Units.instIsScalarTower IsScalarTower.right nonsing_inv_mul smul_smul mul_inv_cancel one_smul
inv_sub_inv 📖	mathematical	IsUnit Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring	Matrix sub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing inv instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	—	nonsing_inv_eq_ringInverse Ring.inverse_sub_inverse
inv_submatrix_equiv 📖	mathematical	—	Matrix inv submatrix DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	IsUnit.nonempty_invertible invOf_eq_nonsing_inv invOf_submatrix_equiv_eq Iff.not isUnit_submatrix_equiv nonsing_inv_eq_ringInverse Ring.inverse_non_unit
inv_subsingleton 📖	mathematical	—	Matrix inv diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ring.inverse Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	inv_def adjugate_subsingleton smul_one_eq_diagonal det_eq_elem_of_subsingleton
inv_zero 📖	mathematical	—	Matrix inv zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	subsingleton_or_nontrivial subsingleton LE.le.eq_or_lt subsingleton_of_empty_right Fintype.card_eq_zero_iff Fintype.card_pos_iff nonsing_inv_apply_not_isUnit AlternatingMap.map_zero NeZero.one
invertibleEquivDetInvertible_apply 📖	mathematical	—	DFunLike.coe Equiv Invertible Matrix instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing det EquivLike.toFunLike Equiv.instEquivLike invertibleEquivDetInvertible detInvertibleOfInvertible	—	—
invertibleEquivDetInvertible_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Invertible Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing det Matrix instMulOfFintypeOfAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass EquivLike.toFunLike Equiv.instEquivLike Equiv.symm invertibleEquivDetInvertible invertibleOfDetInvertible	—	—
isUnit_det_of_invertible 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	—	isUnit_of_invertible
isUnit_det_of_left_inverse 📖	mathematical	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	—	isUnit_of_invertible
isUnit_det_of_right_inverse 📖	mathematical	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	—	isUnit_of_invertible
isUnit_det_transpose 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det transpose	—	det_transpose
isUnit_diagonal 📖	mathematical	—	IsUnit Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.monoid	—	Equiv.nonempty_congr
isUnit_iff_isUnit_det 📖	mathematical	—	IsUnit Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring det	—	Equiv.nonempty_congr
isUnit_nonsing_inv_det 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det Matrix inv	—	IsUnit.of_mul_eq_one instIsDedekindFiniteMonoid det_nonsing_inv_mul_det
isUnit_nonsing_inv_det_iff 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det Matrix inv	—	det_nonsing_inv isUnit_ringInverse
isUnit_nonsing_inv_iff 📖	mathematical	—	IsUnit Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring inv	—	—
isUnit_submatrix_equiv 📖	mathematical	—	IsUnit Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring submatrix DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	Equiv.nonempty_congr
isUnits_det_units 📖	mathematical	—	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det Units.val Matrix semiring	—	isUnit_iff_isUnit_det Units.isUnit
left_inv_eq_left_inv 📖	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—	inv_eq_left_inv
linearIndependent_cols_iff_isUnit 📖	mathematical	—	LinearIndependent col DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Pi.Function.module Semiring.toModule IsUnit Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	row_transpose linearIndependent_rows_iff_isUnit isUnit_transpose
linearIndependent_cols_of_invertible 📖	mathematical	—	LinearIndependent col DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Pi.Function.module Semiring.toModule	—	linearIndependent_cols_iff_isUnit isUnit_of_invertible
linearIndependent_rows_iff_isUnit 📖	mathematical	—	LinearIndependent row DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Pi.Function.module Semiring.toModule IsUnit Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	col_transpose mulVec_injective_iff coe_mulVecLin mulVecLin_transpose vecMul_injective_iff_isUnit coe_vecMulLinear
linearIndependent_rows_of_invertible 📖	mathematical	—	LinearIndependent row DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Pi.Function.module Semiring.toModule	—	linearIndependent_rows_iff_isUnit isUnit_of_invertible
list_prod_inv_reverse 📖	mathematical	—	Matrix inv instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	inv_one List.reverse_cons' Semigroup.to_isLawfulIdentity Semigroup.to_isAssociative mul_inv_rev
mulVec_injective_iff_isUnit 📖	mathematical	—	mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain IsUnit Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	isUnit_transpose vecMul_injective_iff_isUnit vecMul_transpose
mulVec_injective_of_invertible 📖	mathematical	—	mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	mulVec_injective_iff_isUnit isUnit_of_invertible
mulVec_surjective_iff_exists_right_inverse 📖	mathematical	—	mulVec NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	nonempty_fintype ext one_eq_pi_single Pi.single_comm mulVec_mulVec one_mulVec
mulVec_surjective_iff_isUnit 📖	mathematical	—	mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsUnit Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring	—	mulVec_surjective_iff_exists_right_inverse Finite.of_fintype isUnit_iff_exists_inv instIsDedekindFiniteMonoidOfIsStablyFiniteRing instIsStablyFiniteRingOfCommSemiring
mulVec_surjective_of_invertible 📖	mathematical	—	mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	mulVec_surjective_iff_isUnit isUnit_of_invertible
mul_inv_cancel_left_of_invertible 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid inv	—	mul_nonsing_inv_cancel_left isUnit_det_of_invertible
mul_inv_cancel_right_of_invertible 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid inv	—	mul_nonsing_inv_cancel_right isUnit_det_of_invertible
mul_inv_eq_iff_eq_mul_of_invertible 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid inv	—	inv_mul_cancel_right_of_invertible mul_inv_cancel_right_of_invertible
mul_inv_of_invertible 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid inv one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	mul_nonsing_inv isUnit_det_of_invertible
mul_inv_rev 📖	mathematical	—	Matrix inv instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	—	smul_mul IsScalarTower.right mul_smul Algebra.to_smulCommClass smul_smul det_mul adjugate_mul_distrib Ring.mul_inverse_rev
mul_left_inj_of_invertible 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	—	mul_left_injective_of_invertible
mul_left_injective_of_inv 📖	mathematical	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	—	mul_assoc mul_one
mul_left_injective_of_invertible 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	—	mul_inv_cancel_right_of_invertible
mul_nonsing_inv 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid inv one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	IsUnit.nonempty_invertible isUnit_iff_isUnit_det invOf_eq_nonsing_inv mul_invOf_self
mul_nonsing_inv_cancel_left 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid inv	—	mul_nonsing_inv one_mul
mul_nonsing_inv_cancel_right 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid inv	—	mul_assoc mul_nonsing_inv mul_one
mul_right_inj_of_invertible 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	—	mul_right_injective_of_invertible
mul_right_injective_of_inv 📖	mathematical	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	—	one_mul
mul_right_injective_of_invertible 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid	—	inv_mul_cancel_left_of_invertible
nonsing_inv_apply 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	Matrix inv smul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Units Units.instInv IsUnit.unit det adjugate	—	inv_def Ring.inverse_unit IsUnit.unit_spec
nonsing_inv_apply_not_isUnit 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	Matrix inv zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	inv_def Ring.inverse_non_unit zero_smul
nonsing_inv_cancel_or_zero 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid inv one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing zero	—	nonsing_inv_mul mul_nonsing_inv nonsing_inv_apply_not_isUnit
nonsing_inv_eq_ringInverse 📖	mathematical	—	Matrix inv Ring.inverse Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring	—	IsUnit.nonempty_invertible isUnit_iff_isUnit_det invOf_eq_nonsing_inv Ring.inverse_invertible Ring.inverse_non_unit nonsing_inv_apply_not_isUnit
nonsing_inv_mul 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid inv one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	IsUnit.nonempty_invertible isUnit_iff_isUnit_det invOf_eq_nonsing_inv invOf_mul_self
nonsing_inv_mul_cancel_left 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid inv	—	nonsing_inv_mul one_mul
nonsing_inv_mul_cancel_right 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid inv	—	mul_assoc nonsing_inv_mul mul_one
nonsing_inv_nonsing_inv 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	Matrix inv	—	one_mul mul_nonsing_inv mul_assoc isUnit_nonsing_inv_det mul_one
right_inv_eq_left_inv 📖	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—	inv_eq_right_inv inv_eq_left_inv
right_inv_eq_right_inv 📖	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—	inv_eq_right_inv
submatrixEquivInvertibleEquivInvertible_apply 📖	mathematical	—	DFunLike.coe Equiv Invertible Matrix instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing submatrix EquivLike.toFunLike Equiv.instEquivLike submatrixEquivInvertibleEquivInvertible invertibleOfSubmatrixEquivInvertible	—	—
submatrixEquivInvertibleEquivInvertible_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Invertible Matrix instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing submatrix EquivLike.toFunLike Equiv.instEquivLike Equiv.symm submatrixEquivInvertibleEquivInvertible submatrixEquivInvertible	—	—
trace_conj 📖	mathematical	IsUnit Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring	trace NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib inv	—	IsUnit.unit_spec coe_units_inv trace_units_conj
trace_conj' 📖	mathematical	IsUnit Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring	trace NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib inv	—	IsUnit.unit_spec coe_units_inv trace_units_conj'
transpose_nonsing_inv 📖	mathematical	—	transpose Matrix inv	—	inv_def transpose_smul det_transpose adjugate_transpose
unitOfDetInvertible_eq_nonsingInvUnit 📖	mathematical	—	unitOfDetInvertible nonsingInvUnit isUnit_of_invertible MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring det	—	Units.ext isUnit_of_invertible ext
vecMul_injective_iff_isUnit 📖	mathematical	—	vecMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain IsUnit Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	vecMul_surjective_iff_isUnit LinearMap.surjective_of_injective FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.finiteDimensional_self vecMul_injective_of_isUnit
vecMul_injective_of_invertible 📖	mathematical	—	vecMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	vecMul_injective_iff_isUnit isUnit_of_invertible
vecMul_surjective_iff_exists_left_inverse 📖	mathematical	—	vecMul NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid one MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	nonempty_fintype ext mul_apply_eq_vecMul one_eq_pi_single vecMul_vecMul vecMul_one
vecMul_surjective_iff_isUnit 📖	mathematical	—	vecMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsUnit Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring CommSemiring.toSemiring CommRing.toCommSemiring	—	vecMul_surjective_iff_exists_left_inverse Finite.of_fintype isUnit_iff_exists_inv' instIsDedekindFiniteMonoidOfIsStablyFiniteRing instIsStablyFiniteRingOfCommSemiring
vecMul_surjective_of_invertible 📖	mathematical	—	vecMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	vecMul_surjective_iff_isUnit isUnit_of_invertible

Matrix.IsSymm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inv 📖	mathematical	Matrix.IsSymm	Matrix.IsSymm Matrix Matrix.inv	—	smul adjugate

---

← Back to Index