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	113 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, 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	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	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 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 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 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 Algebra.id 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 Algebra.id 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	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 Units.instSMul smul Algebra.toSMul Algebra.id Units.instInv IsUnit.unit	—	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	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	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	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 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 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	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	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	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 📖	—	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	—	—	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 📖	—	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	—	—	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 Algebra.id Units.val Units Units.instInv IsUnit.unit 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 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 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 LinearMap.ker_eq_bot LinearMap.ker_eq_bot' vecMul_vecMul mul_inv_of_invertible vecMul_one map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
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 Matrix.inv	—	smul adjugate

---

← Back to Index