Invertible

📁 Source: Mathlib/Data/Matrix/Invertible.lean

Statistics

Metric	Count
Definitions `Invertible`, `invertibleAddMulMul`, `invertibleAddMulMul'`, `invertibleConjTranspose`, `invertibleOfInvertibleConjTranspose`, `invertibleOfInvertibleTranspose`, `invertibleTranspose`, `transposeInvertibleEquivInvertible`, `Invertible`	9
Theorems `add_mul_mul_invOf_mul_eq_one`, `add_mul_mul_invOf_mul_eq_one'`, `add_mul_mul_mul_invOf_eq_one`, `add_mul_mul_mul_invOf_eq_one'`, `conjTranspose_invOf`, `invOf_add_mul_mul`, `invOf_add_mul_mul'`, `invOf_mul_cancel_left`, `invOf_mul_cancel_right`, `invOf_mul_eq_iff_eq_mul_left`, `isUnit_conjTranspose`, `isUnit_transpose`, `mul_invOf_cancel_left`, `mul_invOf_cancel_right`, `mul_invOf_eq_iff_eq_mul_right`, `mul_left_eq_iff_eq_invOf_mul`, `mul_right_eq_iff_eq_mul_invOf`, `transposeInvertibleEquivInvertible_apply`, `transposeInvertibleEquivInvertible_symm_apply`, `transpose_invOf`	20
Total	29

Matrix

Definitions

Name	Category	Theorems
`invertibleAddMulMul` 📖	CompOp	—
`invertibleAddMulMul'` 📖	CompOp	—
`invertibleConjTranspose` 📖	CompOp	—
`invertibleOfInvertibleConjTranspose` 📖	CompOp	—
`invertibleOfInvertibleTranspose` 📖	CompOp	1 math math: `transposeInvertibleEquivInvertible_apply`
`invertibleTranspose` 📖	CompOp	1 math math: `transposeInvertibleEquivInvertible_symm_apply`
`transposeInvertibleEquivInvertible` 📖	CompOp	2 math math: `transposeInvertibleEquivInvertible_symm_apply`, `transposeInvertibleEquivInvertible_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_mul_mul_invOf_mul_eq_one` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `add` `Distrib.toAdd` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Invertible.invOf` `instMulOfFintypeOfAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`add_sub_assoc` `add_mul` `Distrib.rightDistribClass` `mul_sub` `mul_assoc` `mul_invOf_self` `one_mul` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.const_add_termg` `add_mul` `mul_add` `mul_invOf_cancel_right` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Tactic.Abel.zero_termg`
`add_mul_mul_invOf_mul_eq_one'` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Invertible.invOf` `instMulOfFintypeOfAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `add` `Distrib.toAdd`	—	`add_sub_assoc` `mul_add` `Distrib.leftDistribClass` `sub_mul` `mul_assoc` `invOf_mul_self` `invOf_mul_cancel_right` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.const_add_termg` `mul_add` `add_mul` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Tactic.Abel.zero_termg`
`add_mul_mul_mul_invOf_eq_one` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `add` `Distrib.toAdd` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Invertible.invOf` `instMulOfFintypeOfAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`mul_sub` `add_mul` `mul_invOf_self'` `add_sub_assoc` `add_eq_left` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `sub_eq_zero` `one_mul` `mul_right_eq_iff_eq_mul_invOf` `mul_assoc` `mul_add`
`add_mul_mul_mul_invOf_eq_one'` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Invertible.invOf` `instMulOfFintypeOfAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `add` `Distrib.toAdd`	—	`mul_add` `sub_mul` `invOf_mul_self'` `sub_add` `sub_eq_self` `sub_eq_zero` `mul_assoc` `eq_sub_iff_add_eq` `invOf_mul_eq_iff_eq_mul_left` `mul_one` `add_mul` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`conjTranspose_invOf` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `Invertible.invOf` `Matrix` `instMulOfFintypeOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`star_invOf`
`invOf_add_mul_mul` 📖	mathematical	—	`Invertible.invOf` `Matrix` `instMulOfFintypeOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `add` `Distrib.toAdd` `instHMulOfFintypeOfMulOfAddCommMonoid` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup`	—	`Invertible.congr`
`invOf_add_mul_mul'` 📖	mathematical	—	`Invertible.invOf` `Matrix` `instMulOfFintypeOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `add` `Distrib.toAdd` `instHMulOfFintypeOfMulOfAddCommMonoid` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup`	—	`Invertible.congr`
`invOf_mul_cancel_left` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Invertible.invOf` `instMulOfFintypeOfAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`mul_assoc` `invOf_mul_self` `one_mul`
`invOf_mul_cancel_right` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Invertible.invOf` `instMulOfFintypeOfAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`mul_assoc` `invOf_mul_self` `mul_one`
`invOf_mul_eq_iff_eq_mul_left` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Invertible.invOf` `instMulOfFintypeOfAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`mul_invOf_cancel_left` `invOf_mul_cancel_left`
`isUnit_conjTranspose` 📖	mathematical	—	`IsUnit` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid`	—	`isUnit_star`
`isUnit_transpose` 📖	mathematical	—	`IsUnit` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `CommSemiring.toSemiring` `transpose`	—	`Equiv.nonempty_congr`
`mul_invOf_cancel_left` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Invertible.invOf` `instMulOfFintypeOfAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`mul_assoc` `mul_invOf_self` `one_mul`
`mul_invOf_cancel_right` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Invertible.invOf` `instMulOfFintypeOfAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`mul_assoc` `mul_invOf_self` `mul_one`
`mul_invOf_eq_iff_eq_mul_right` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Invertible.invOf` `instMulOfFintypeOfAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`invOf_mul_cancel_right` `mul_invOf_cancel_right`
`mul_left_eq_iff_eq_invOf_mul` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Invertible.invOf` `instMulOfFintypeOfAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`invOf_mul_eq_iff_eq_mul_left`
`mul_right_eq_iff_eq_mul_invOf` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Invertible.invOf` `instMulOfFintypeOfAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`mul_invOf_eq_iff_eq_mul_right`
`transposeInvertibleEquivInvertible_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Invertible` `Matrix` `instMulOfFintypeOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `transpose` `EquivLike.toFunLike` `Equiv.instEquivLike` `transposeInvertibleEquivInvertible` `invertibleOfInvertibleTranspose`	—	—
`transposeInvertibleEquivInvertible_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Invertible` `Matrix` `instMulOfFintypeOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `transpose` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `transposeInvertibleEquivInvertible` `invertibleTranspose`	—	—
`transpose_invOf` 📖	mathematical	—	`transpose` `Invertible.invOf` `Matrix` `instMulOfFintypeOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Invertible.congr`

Module

Definitions

Name	Category	Theorems
`Invertible` 📖	CompData	15 math math: `Invertible.instTensorProduct_1`, `Invertible.inst`, `instInvertibleCarrierOutSemimoduleCatValSkeleton`, `Invertible.instDual`, `Invertible.instTensorProduct_2`, `Invertible.congr`, `instInvertibleReprₛ`, `Submodule.instInvertibleSubtypeMemVal`, `Invertible.of_isLocalization`, `Invertible.instLocalizationLocalizedModule`, `Invertible.instTensorProduct`, `Invertible.left`, `instInvertibleCarrierOutModuleCatValSkeleton`, `Flat.instInvertibleSubtypeMemSubmoduleSubmoduleAlgebra`, `Invertible.right`

(root)

Definitions

Name	Category	Theorems
`Invertible` 📖	CompData	21 math math: `Matrix.transposeInvertibleEquivInvertible_symm_apply`, `Invertible.subsingleton`, `Invertible.mulRight_apply`, `TrivSqZeroExt.invertibleEquivInvertibleFst_symm_apply_invOf`, `Invertible.mulLeft_apply`, `ExteriorAlgebra.invertibleAlgebraMapEquiv_apply_invOf`, `IsUnit.nonempty_invertible`, `TrivSqZeroExt.invertibleEquivInvertibleFst_apply_invOf`, `Invertible.mulLeft_symm_apply`, `invertibleEquivOfLeftInverse_apply`, `Matrix.submatrixEquivInvertibleEquivInvertible_apply`, `Matrix.diagonalInvertibleEquivInvertible_symm_apply`, `Matrix.diagonalInvertibleEquivInvertible_apply`, `Matrix.invertibleEquivDetInvertible_apply`, `nonempty_invertible_iff_isUnit`, `Matrix.invertibleEquivDetInvertible_symm_apply`, `Matrix.submatrixEquivInvertibleEquivInvertible_symm_apply`, `Invertible.mulRight_symm_apply`, `ExteriorAlgebra.invertibleAlgebraMapEquiv_symm_apply_invOf_toQuot`, `Matrix.transposeInvertibleEquivInvertible_apply`, `invertibleEquivOfLeftInverse_symm_apply`

---

← Back to Index