Documentation Verification Report

LocalizationLocalization

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

Statistics

Metric	Count
Definitions `instAlgebraAtPrimeLocalization`, `instAlgebraLocalizationAtPrime`, `localizationAlgebraOfSubmonoidLe`, `localizationLocalizationAtPrimeIsoLocalization`, `localizationLocalizationSubmodule`	5
Theorems `instAtPrimeFractionRing`, `isFractionRing_of_isDomain_of_isLocalization`, `isFractionRing_of_isLocalization`, `instIsScalarTowerAtPrimeFractionRing`, `instIsScalarTowerLocalizationAtPrime`, `isLocalization_atPrime_localization_atPrime`, `isLocalization_isLocalization_atPrime_isLocalization`, `isLocalization_of_is_exists_mul_mem`, `isLocalization_of_submonoid_le`, `localization_isScalarTower_of_submonoid_le`, `localization_localization_exists_of_eq`, `localization_localization_isLocalization`, `localization_localization_isLocalization_of_has_all_units`, `localization_localization_map_units`, `localization_localization_surj`, `mem_localizationLocalizationSubmodule`, `mk'_eq_algebraMap_mk'_of_submonoid_le`	17
Total	22

IsFractionRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instAtPrimeFractionRing` 📖	mathematical	—	`IsFractionRing` `Localization.AtPrime` `CommRing.toCommSemiring` `OreLocalization.instCommSemiring` `Ideal.primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `FractionRing` `nonZeroDivisors` `Semiring.toMonoidWithZero` `CommRing.toCommMonoid` `IsLocalization.instAlgebraLocalizationAtPrime`	—	`isFractionRing_of_isDomain_of_isLocalization` `IsLocalization.instIsScalarTowerAtPrimeFractionRing` `Localization.isLocalization`
`isFractionRing_of_isDomain_of_isLocalization` 📖	mathematical	—	`IsFractionRing` `CommRing.toCommSemiring`	—	`isFractionRing_of_isLocalization` `mem_nonZeroDivisors_iff_ne_zero` `IsDomain.to_noZeroDivisors` `IsDomain.toNontrivial` `zero_ne_one` `NeZero.one` `RingHom.domain_nontrivial` `nontrivial` `RingHom.map_one` `IsLocalization.mk'_one` `comm` `IsEquiv.toSymm` `eq_isEquiv` `IsLocalization.mk'_eq_zero_iff` `mul_one`
`isFractionRing_of_isLocalization` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Semiring.toMonoidWithZero`	`IsFractionRing`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsLocalization.isLocalization_of_submonoid_le` `IsLocalization.isLocalization_of_is_exists_mul_mem` `IsLocalization.map_nonZeroDivisors_le` `IsLocalization.surj` `mul_comm` `Set.mem_image_of_mem` `mem_nonZeroDivisors_iff_right` `IsLocalization.injective` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `IsLocalization.map_units` `mul_assoc` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `MulZeroClass.zero_mul`

IsLocalization

Definitions

Name	Category	Theorems
`instAlgebraAtPrimeLocalization` 📖	CompOp	1 math math: `isLocalization_atPrime_localization_atPrime`
`instAlgebraLocalizationAtPrime` 📖	CompOp	3 math math: `instIsFractionRingAtPrimeFractionRing`, `IsFractionRing.instAtPrimeFractionRing`, `instIsScalarTowerAtPrimeFractionRing`
`localizationAlgebraOfSubmonoidLe` 📖	CompOp	1 math math: `localization_isScalarTower_of_submonoid_le`
`localizationLocalizationAtPrimeIsoLocalization` 📖	CompOp	—
`localizationLocalizationSubmodule` 📖	CompOp	5 math math: `localization_localization_surj`, `localization_localization_map_units`, `mem_localizationLocalizationSubmodule`, `localization_localization_exists_of_eq`, `localization_localization_isLocalization`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsScalarTowerAtPrimeFractionRing` 📖	mathematical	—	`IsScalarTower` `Localization.AtPrime` `CommRing.toCommSemiring` `FractionRing` `OreLocalization.instSMulOfIsScalarTower` `CommMonoid.toMonoid` `CommSemiring.toCommMonoid` `Ideal.primeCompl` `CommSemiring.toSemiring` `OreLocalization.oreSetComm` `Monoid.toMulAction` `Algebra.toSMul` `Algebra.id` `IsScalarTower.right` `OreLocalization.instCommSemiring` `OreLocalization.instSemiring` `nonZeroDivisors` `Semiring.toMonoidWithZero` `instAlgebraLocalizationAtPrime` `CommRing.toCommMonoid`	—	`localization_isScalarTower_of_submonoid_le` `Ideal.primeCompl_le_nonZeroDivisors` `IsDomain.to_noZeroDivisors` `Localization.isLocalization`
`instIsScalarTowerLocalizationAtPrime` 📖	mathematical	—	`IsScalarTower` `Localization` `CommSemiring.toCommMonoid` `Localization.AtPrime` `OreLocalization.instCommSemiring` `OreLocalization.oreSetComm` `OreLocalization.instSMulOfIsScalarTower` `CommMonoid.toMonoid` `Monoid.toMulAction` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right` `Ideal.primeCompl` `OreLocalization.instSMul` `OreLocalization.instSemiring` `OreLocalization.instAlgebra`	—	`IsScalarTower.of_algebraMap_eq'`
`isLocalization_atPrime_localization_atPrime` 📖	mathematical	—	`AtPrime` `Localization.AtPrime` `Localization` `CommSemiring.toCommMonoid` `OreLocalization.instCommSemiring` `OreLocalization.oreSetComm` `Ideal.primeCompl` `CommSemiring.toSemiring` `instAlgebraAtPrimeLocalization` `Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `OreLocalization.instSemiring` `RingHom.instFunLike` `algebraMap` `OreLocalization.instAlgebra` `Algebra.id` `RingHom.instRingHomClass` `Ideal.IsPrime.under`	—	`isLocalization_isLocalization_atPrime_isLocalization` `instIsScalarTowerLocalizationAtPrime` `Localization.isLocalization`
`isLocalization_isLocalization_atPrime_isLocalization` 📖	mathematical	—	`AtPrime` `Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `RingHom.instRingHomClass` `Ideal.IsPrime.under`	—	`localization_localization_isLocalization_of_has_all_units` `Ideal.IsPrime.ne_top'` `Ideal.eq_top_of_isUnit_mem`
`isLocalization_of_is_exists_mul_mem` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `SetLike.instMembership` `Submonoid.instSetLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	`IsLocalization`	—	`map_units` `IsUnit.mul_iff` `instIsDedekindFiniteMonoid` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `surj` `Subtype.prop` `eq_iff_exists`
`isLocalization_of_submonoid_le` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder`	`IsLocalization` `Submonoid.map` `RingHom` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `algebraMap`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsScalarTower.algebraMap_apply` `map_units` `surj` `Subtype.prop` `Set.exists_image_iff` `eq_iff_exists` `one_mul` `mul_comm` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `mul_right_comm`
`localization_isScalarTower_of_submonoid_le` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder`	`IsScalarTower` `Algebra.toSMul` `localizationAlgebraOfSubmonoidLe`	—	`IsScalarTower.of_algebraMap_eq'` `lift_comp`
`localization_localization_exists_of_eq` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `localizationLocalizationSubmodule`	—	`IsScalarTower.algebraMap_apply` `eq_iff_exists` `surj` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `mul_assoc` `mul_comm` `mem_localizationLocalizationSubmodule` `Submonoid.coe_mul` `mul_left_comm`
`localization_localization_isLocalization` 📖	mathematical	—	`IsLocalization` `localizationLocalizationSubmodule`	—	`localization_localization_map_units` `localization_localization_surj` `localization_localization_exists_of_eq`
`localization_localization_isLocalization_of_has_all_units` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike`	`IsLocalization` `Submonoid.comap` `RingHom` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `algebraMap`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `sup_eq_left` `map_units` `localization_localization_isLocalization`
`localization_localization_map_units` 📖	mathematical	—	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `localizationLocalizationSubmodule`	—	`mem_localizationLocalizationSubmodule` `Subtype.prop` `IsScalarTower.algebraMap_apply` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `IsUnit.mul_iff` `instIsDedekindFiniteMonoid` `map_units` `IsUnit.map` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass`
`localization_localization_surj` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `localizationLocalizationSubmodule`	—	`surj` `mem_localizationLocalizationSubmodule` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `mul_assoc` `SubmonoidClass.toMulMemClass` `Submonoid.instSubmonoidClass` `mul_comm` `Submonoid.coe_mul` `IsScalarTower.algebraMap_apply` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul`
`mem_localizationLocalizationSubmodule` 📖	mathematical	—	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `localizationLocalizationSubmodule` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`localizationLocalizationSubmodule.eq_1` `Submonoid.mem_comap` `Submonoid.mem_sup` `Subtype.prop`
`mk'_eq_algebraMap_mk'_of_submonoid_le` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder`	`mk'` `SetLike.instMembership` `Submonoid.instSetLike` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`mk'_eq_iff_eq_mul` `IsScalarTower.algebraMap_apply` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `mk'_spec`

---

← Back to Index