Documentation Verification Report

InvSubmonoid

📁 Source: Mathlib/RingTheory/Localization/InvSubmonoid.lean

Statistics

Metric	Count
Definitions `equivInvSubmonoid`, `invSubmonoid`, `toInvSubmonoid`	3
Theorems `finiteType_of_monoid_fg`, `instFiniteTypeLocalizationOfFGSubtypeMemSubmonoid`, `mem_invSubmonoid_iff_exists_mk'`, `mul_toInvSubmonoid`, `smul_toInvSubmonoid`, `span_invSubmonoid`, `submonoid_map_le_is_unit`, `surj''`, `toInvSubmonoid_eq_mk'`, `toInvSubmonoid_mul`, `toInvSubmonoid_surjective`	11
Total	14

IsLocalization

Definitions

Name	Category	Theorems
`equivInvSubmonoid` 📖	CompOp	—
`invSubmonoid` 📖	CompOp	8 math math: `surj''`, `mem_invSubmonoid_iff_exists_mk'`, `toInvSubmonoid_mul`, `toInvSubmonoid_surjective`, `toInvSubmonoid_eq_mk'`, `mul_toInvSubmonoid`, `span_invSubmonoid`, `smul_toInvSubmonoid`
`toInvSubmonoid` 📖	CompOp	6 math math: `surj''`, `toInvSubmonoid_mul`, `toInvSubmonoid_surjective`, `toInvSubmonoid_eq_mk'`, `mul_toInvSubmonoid`, `smul_toInvSubmonoid`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finiteType_of_monoid_fg` 📖	mathematical	—	`Algebra.FiniteType` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	—	`Monoid.fg_of_surjective` `toInvSubmonoid_surjective` `Monoid.fg_iff_submonoid_fg` `eq_top_iff` `Algebra.adjoin_eq_span` `span_invSubmonoid`
`instFiniteTypeLocalizationOfFGSubtypeMemSubmonoid` 📖	mathematical	—	`Algebra.FiniteType` `Localization` `CommRing.toCommMonoid` `CommRing.toCommSemiring` `OreLocalization.instSemiring` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `OreLocalization.instAlgebra`	—	`Algebra.FiniteType.trans` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `finiteType_of_monoid_fg` `Localization.isLocalization`
`mem_invSubmonoid_iff_exists_mk'` 📖	mathematical	—	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `invSubmonoid` `mk'` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`toInvSubmonoid_surjective` `Subtype.prop`
`mul_toInvSubmonoid` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `invSubmonoid` `MonoidHom` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `MonoidHom.instFunLike` `toInvSubmonoid` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Submonoid.mul_leftInvEquiv_symm` `submonoid_map_le_is_unit`
`smul_toInvSubmonoid` 📖	mathematical	—	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.smul` `Algebra.toSMul` `invSubmonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `MonoidHom.instFunLike` `toInvSubmonoid` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Algebra.smul_def` `mul_toInvSubmonoid`
`span_invSubmonoid` 📖	mathematical	—	`Submodule.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `SetLike.coe` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Submonoid.instSetLike` `invSubmonoid` `Top.top` `Submodule` `Submodule.instTop`	—	`eq_top_iff` `surj''` `Submodule.smul_mem` `Submodule.subset_span` `Subtype.prop`
`submonoid_map_le_is_unit` 📖	mathematical	—	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `Submonoid.map` `RingHom` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `algebraMap` `IsUnit.submonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_units`
`surj''` 📖	mathematical	—	`Algebra.toSMul` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `invSubmonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `MonoidHom.instFunLike` `toInvSubmonoid`	—	`surj` `Algebra.smul_def` `mul_assoc` `mul_toInvSubmonoid` `mul_one`
`toInvSubmonoid_eq_mk'` 📖	mathematical	—	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `invSubmonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `MonoidHom.instFunLike` `toInvSubmonoid` `mk'` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`map_units` `toInvSubmonoid_mul` `mk'_spec` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`toInvSubmonoid_mul` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `invSubmonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `MonoidHom.instFunLike` `toInvSubmonoid` `RingHom` `RingHom.instFunLike` `algebraMap` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Submonoid.leftInvEquiv_symm_mul` `submonoid_map_le_is_unit`
`toInvSubmonoid_surjective` 📖	mathematical	—	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `invSubmonoid` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `MonoidHom.instFunLike` `toInvSubmonoid`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Equiv.surjective` `MonoidHom.submonoidMap_surjective`

---

← Back to Index