Documentation Verification Report

SemiringInverse

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

Statistics

Metric	Count
Definitions `adjp`, `detp`, `invertibleOfLeftInverse`, `invertibleOfRightInverse`	4
Theorems `adjp_apply`, `detp_mul`, `detp_neg_one_one`, `detp_one_one`, `detp_smul_add_adjp`, `detp_smul_adjp`, `exists_left_inverse_iff_isUnit`, `exists_right_inverse_iff_isUnit`, `instIsStablyFiniteRingOfCommSemiring`, `isAddUnit_detp_mul_detp`, `isAddUnit_detp_smul_mul_adjp`, `isAddUnit_mul`, `isUnit_of_left_inverse`, `isUnit_of_right_inverse`, `mul_adjp_add_detp`, `mul_adjp_apply_eq`, `mul_adjp_apply_ne`, `mul_eq_one_comm`	18
Total	22

Matrix

Definitions

Name	Category	Theorems
`adjp` 📖	CompOp	7 math math: `adjp_apply`, `mul_adjp_apply_eq`, `detp_smul_adjp`, `detp_smul_add_adjp`, `isAddUnit_detp_smul_mul_adjp`, `mul_adjp_apply_ne`, `mul_adjp_add_detp`
`detp` 📖	CompOp	10 math math: `detp_neg_one_one`, `detp_one_one`, `det_eq_detp_sub_detp`, `mul_adjp_apply_eq`, `detp_smul_adjp`, `detp_smul_add_adjp`, `isAddUnit_detp_smul_mul_adjp`, `detp_mul`, `mul_adjp_add_detp`, `isAddUnit_detp_mul_detp`
`invertibleOfLeftInverse` 📖	CompOp	—
`invertibleOfRightInverse` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjp_apply` 📖	mathematical	—	`adjp` `Finset.sum` `Equiv.Perm` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finset.filter` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.Perm.ofSign` `Finset.prod` `CommSemiring.toCommMonoid` `Compl.compl` `Finset` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `Finset.instSingleton`	—	—
`detp_mul` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `detp` `Units` `Int.instMonoid` `Units.instOne` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing`	—	`RightCancelSemigroup.toIsRightCancelMul` `Finset.ext` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `map_inv` `Equiv.Perm.mem_ofSign` `Finset.sum_mul_sum` `Finset.sum_congr` `Finset.prod_mul_distrib` `Finset.sum_map` `Finset.prod_congr` `Equiv.prod_comp` `Equiv.coe_fn_injective` `Equiv.Perm.ofSign_disjoint` `neg_mul_neg` `mul_one` `Finset.prod_univ_sum` `Finset.sum_comm` `Finset.sum_compl_add_sum` `Finset.sum_disjUnion` `neg_neg` `add_assoc` `Mathlib.Tactic.Contrapose.contrapose₃` `Finset.notMem_compl` `Finset.mem_map` `Equiv.Perm.ofSign_disjUnion` `Function.Injective.bijective_of_finite` `Finite.of_fintype` `Finset.mem_univ` `Function.not_injective_iff` `Equiv.swap_apply_def` `mul_neg_one` `Equiv.Perm.sign_swap` `add_comm`
`detp_neg_one_one` 📖	mathematical	—	`detp` `Units` `Int.instMonoid` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `Units.instOne` `Matrix` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`detp.eq_1` `Finset.sum_eq_zero` `Mathlib.Tactic.Contrapose.contrapose₃` `Equiv.Perm.mem_ofSign` `Equiv.Perm.sign_one` `Equiv.Perm.ext_iff` `Finset.prod_eq_zero` `Finset.mem_univ` `one_apply_ne'`
`detp_one_one` 📖	mathematical	—	`detp` `Units` `Int.instMonoid` `Units.instOne` `Matrix` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`detp.eq_1` `Finset.sum_eq_single_of_mem` `Equiv.Perm.sign_one` `Equiv.Perm.ext_iff` `Finset.prod_eq_zero` `Finset.mem_univ` `one_apply_ne'` `Finset.prod_congr` `Finset.prod_const_one`
`detp_smul_add_adjp` 📖	mathematical	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`add` `Distrib.toAdd` `smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `DistribSMul.toSMulZeroClass` `instDistribSMul` `detp` `Units` `Int.instMonoid` `Units.instOne` `adjp` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing`	—	`mul_adjp_add_detp` `add_comm` `mul_one` `mul_smul` `smulCommClass_self` `one_mul` `mul_add` `Distrib.leftDistribClass`
`detp_smul_adjp` 📖	mathematical	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`add` `Distrib.toAdd` `smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `DistribSMul.toSMulZeroClass` `instDistribSMul` `detp` `Units` `Int.instMonoid` `Units.instOne` `adjp` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing`	—	`detp_mul` `detp_smul_add_adjp` `IsAddUnit.smul_right` `isAddUnit_detp_mul_detp` `add_assoc` `add_comm` `one_smul` `add_smul` `zero_add` `detp_neg_one_one` `detp_one_one` `add_add_add_comm` `smul_add` `smul_smul`
`exists_left_inverse_iff_isUnit` 📖	mathematical	—	`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` `IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring`	—	`isUnit_iff_exists_inv'` `instIsDedekindFiniteMonoidOfIsStablyFiniteRing` `instIsStablyFiniteRingOfCommSemiring`
`exists_right_inverse_iff_isUnit` 📖	mathematical	—	`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` `IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring`	—	`isUnit_iff_exists_inv` `instIsDedekindFiniteMonoidOfIsStablyFiniteRing` `instIsStablyFiniteRingOfCommSemiring`
`instIsStablyFiniteRingOfCommSemiring` 📖	mathematical	—	`IsStablyFiniteRing` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`detp_mul` `detp_smul_adjp` `mul_add` `Distrib.leftDistribClass` `mul_smul` `smulCommClass_self` `IsAddUnit.add` `isAddUnit_detp_smul_mul_adjp` `IsAddUnit.smul_right` `isAddUnit_detp_mul_detp` `add_smul` `smul_smul` `add_add_add_comm` `smul_add` `add_assoc` `add_comm` `one_smul` `zero_add` `detp_neg_one_one` `detp_one_one` `mul_adjp_add_detp`
`isAddUnit_detp_mul_detp` 📖	mathematical	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`IsAddUnit` `AddMonoidWithOne.toAddMonoid` `Distrib.toAdd` `detp` `Units` `Int.instMonoid` `Units.instOne` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing`	—	`Finset.sum_mul_sum` `Equiv.Perm.sign_inv` `Equiv.Perm.mem_ofSign` `eq_inv_iff_mul_eq_one` `mul_comm` `Equiv.prod_comp` `Finset.prod_mul_distrib` `Finset.mul_prod_erase` `Finset.mem_univ` `smul_eq_mul` `IsAddUnit.smul_right` `isAddUnit_mul` `IsAddUnit.add`
`isAddUnit_detp_smul_mul_adjp` 📖	mathematical	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`IsAddUnit` `addMonoid` `AddMonoidWithOne.toAddMonoid` `add` `Distrib.toAdd` `smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `instDistribSMul` `detp` `Units` `Int.instMonoid` `Units.instOne` `adjp` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing`	—	`isAddUnit_iff` `Finset.sum_congr` `Finset.mul_sum` `Finset.sum_mul` `Equiv.Perm.sign_inv` `Equiv.Perm.mem_ofSign` `Finset.mem_filter` `Finset.exists_mem_ne` `Equiv.Perm.one_lt_card_support_of_ne_one` `eq_inv_iff_mul_eq_one` `Finset.prod_mul_prod_compl` `mul_mul_mul_comm` `mul_comm` `smul_eq_mul` `IsAddUnit.smul_right` `Finset.prod_equiv` `Finset.prod_mul_distrib` `Finset.mul_prod_erase` `Finset.mem_compl` `Finset.mem_singleton` `isAddUnit_mul` `Equiv.Perm.mem_support` `IsAddUnit.add`
`isAddUnit_mul` 📖	mathematical	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`IsAddUnit` `AddMonoidWithOne.toAddMonoid`	—	`IsAddUnit.sum_univ_iff` `mul_apply` `one_apply_ne` `isAddUnit_zero`
`isUnit_of_left_inverse` 📖	mathematical	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring`	—	`IsUnit.of_mul_eq_one_right` `instIsDedekindFiniteMonoidOfIsStablyFiniteRing` `instIsStablyFiniteRingOfCommSemiring`
`isUnit_of_right_inverse` 📖	mathematical	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring`	—	`IsUnit.of_mul_eq_one` `instIsDedekindFiniteMonoidOfIsStablyFiniteRing` `instIsStablyFiniteRingOfCommSemiring`
`mul_adjp_add_detp` 📖	mathematical	—	`Matrix` `add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `adjp` `Units` `Int.instMonoid` `Units.instOne` `smul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `instDistribSMul` `detp` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne`	—	`ext` `eq_or_ne` `mul_adjp_apply_eq` `one_apply_eq` `mul_one` `add_comm` `mul_adjp_apply_ne` `one_apply_ne` `MulZeroClass.mul_zero`
`mul_adjp_apply_eq` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `adjp` `detp`	—	`Finset.sum_fiberwise_eq_sum_filter` `Finset.sum_congr` `Finset.mul_sum` `Finset.filter_true` `Finset.filter.congr_simp` `Finset.prod_mul_prod_compl` `Finset.prod_singleton` `Finset.mem_filter`
`mul_adjp_apply_ne` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `adjp` `Units` `Int.instMonoid` `Units.instOne` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing`	—	`Finset.sum_congr` `Finset.mul_sum` `Finset.sum_sigma'` `Equiv.swap_apply_left` `Equiv.Perm.mem_ofSign` `Finset.mem_filter` `Finset.mem_sigma` `Equiv.mul_swap_mul_self` `Finset.sum_bij'` `Equiv.Perm.mul_apply` `Equiv.Perm.sign_mul` `Equiv.Perm.sign_swap` `Equiv.swap_apply_right` `Finset.mem_univ` `Finset.compl_insert` `Finset.disjoint_singleton_left` `Finset.singleton_disjUnion` `Finset.cons_eq_insert` `Finset.insert_erase` `Finset.mem_compl` `Finset.mem_singleton` `Finset.prod_congr` `Finset.prod_disjUnion` `Finset.prod_singleton` `mul_comm` `Equiv.swap_apply_of_ne_of_ne` `Finset.mem_insert`
`mul_eq_one_comm` 📖	mathematical	—	`MulOne.toMul` `MulOne.toOne`	—	`mul_eq_one_comm`

---

← Back to Index