Documentation Verification Report

LocalSubring

📁 Source: Mathlib/RingTheory/LocalRing/LocalSubring.lean

Statistics

Metric	Count
Definitions `copy`, `instAlgebraSubtypeMemSubringToSubringOfPrime`, `instPartialOrder`, `map`, `ofPrime`, `ofPrimeEquiv`, `range`, `toSubring`	8
Theorems `ext`, `ext_iff`, `instAtPrimeSubtypeMemSubringToSubringOfPrime`, `instIsScalarTowerSubtypeMemSubringToSubringOfPrime`, `isLocalRing`, `le_def`, `le_ofPrime`, `map_toSubring`, `range_toSubring`, `toSubring_injective`, `toSubring_mono`, `instIsLocalRingSubtypeMemSubringMapOfNontrivial`, `isLocalRing_top`	13
Total	21

LocalSubring

Definitions

Name	Category	Theorems
`copy` 📖	CompOp	—
`instAlgebraSubtypeMemSubringToSubringOfPrime` 📖	CompOp	2 math math: `instAtPrimeSubtypeMemSubringToSubringOfPrime`, `instIsScalarTowerSubtypeMemSubringToSubringOfPrime`
`instPartialOrder` 📖	CompOp	7 math math: `isMax_iff`, `ValuationSubring.isMax_toLocalSubring`, `toSubring_mono`, `exists_le_valuationSubring`, `exists_le_valuationSubring_of_isIntegrallyClosedIn`, `eq_iInf_of_isIntegrallyClosedIn`, `le_def`
`map` 📖	CompOp	1 math math: `map_toSubring`
`ofPrime` 📖	CompOp	3 math math: `instAtPrimeSubtypeMemSubringToSubringOfPrime`, `le_ofPrime`, `instIsScalarTowerSubtypeMemSubringToSubringOfPrime`
`ofPrimeEquiv` 📖	CompOp	—
`range` 📖	CompOp	1 math math: `range_toSubring`
`toSubring` 📖	CompOp	11 math math: `isLocalRing`, `range_toSubring`, `toSubring_mono`, `eq_iInf_of_isIntegrallyClosedIn`, `instAtPrimeSubtypeMemSubringToSubringOfPrime`, `map_toSubring`, `le_ofPrime`, `ext_iff`, `instIsScalarTowerSubtypeMemSubringToSubringOfPrime`, `le_def`, `toSubring_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`toSubring`	—	—	`SubringClass.toSubsemiringClass` `Subring.instSubringClass`
`ext_iff` 📖	mathematical	—	`toSubring`	—	`ext`
`instAtPrimeSubtypeMemSubringToSubringOfPrime` 📖	mathematical	—	`IsLocalization.AtPrime` `Subring` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subring.instSetLike` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `CommRing.toRing` `Field.toCommRing` `toSubring` `ofPrime` `instAlgebraSubtypeMemSubringToSubringOfPrime`	—	`SubringClass.toSubsemiringClass` `Subring.instSubringClass` `IsLocalization.isLocalization_of_algEquiv` `Localization.isLocalization`
`instIsScalarTowerSubtypeMemSubringToSubringOfPrime` 📖	mathematical	—	`IsScalarTower` `Subring` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subring.instSetLike` `CommRing.toRing` `Field.toCommRing` `toSubring` `ofPrime` `Algebra.toSMul` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `CommSemiring.toSemiring` `instAlgebraSubtypeMemSubringToSubringOfPrime` `Subring.instSMulSubtypeMem` `Algebra.id`	—	`SubringClass.toSubsemiringClass` `Subring.instSubringClass` `IsScalarTower.of_algebraMap_eq`
`isLocalRing` 📖	mathematical	—	`IsLocalRing` `Subring` `CommRing.toRing` `SetLike.instMembership` `Subring.instSetLike` `toSubring` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `CommRing.toCommSemiring` `SubringClass.toSubsemiringClass` `Subring.instSubringClass`	—	—
`le_def` 📖	mathematical	—	`LocalSubring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IsLocalHom` `Subring` `CommRing.toRing` `SetLike.instMembership` `Subring.instSetLike` `toSubring` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Subring.toRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `CommRing.toCommSemiring` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `RingHom.instFunLike` `Subring.inclusion`	—	—
`le_ofPrime` 📖	mathematical	—	`Subring` `DivisionRing.toRing` `Field.toDivisionRing` `Preorder.toLE` `PartialOrder.toPreorder` `Subring.instPartialOrder` `toSubring` `Field.toCommRing` `ofPrime`	—	`SubringClass.toSubsemiringClass` `Subring.instSubringClass` `IsLocalization.lift_eq`
`map_toSubring` 📖	mathematical	—	`toSubring` `map` `Subring.map` `CommRing.toRing`	—	—
`range_toSubring` 📖	mathematical	—	`toSubring` `range` `Subring.copy` `CommRing.toRing` `Subring.map` `Top.top` `Subring` `Subring.instTop` `Set.range` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `RingHom.instFunLike`	—	—
`toSubring_injective` 📖	mathematical	—	`LocalSubring` `Subring` `CommRing.toRing` `toSubring`	—	`SubringClass.toSubsemiringClass` `Subring.instSubringClass`
`toSubring_mono` 📖	mathematical	—	`Monotone` `LocalSubring` `Subring` `CommRing.toRing` `PartialOrder.toPreorder` `instPartialOrder` `Subring.instPartialOrder` `toSubring`	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsLocalRingSubtypeMemSubringMapOfNontrivial` 📖	mathematical	—	`IsLocalRing` `Subring` `CommRing.toRing` `SetLike.instMembership` `Subring.instSetLike` `Subring.map` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `CommRing.toCommSemiring` `SubringClass.toSubsemiringClass` `Subring.instSubringClass`	—	`SubringClass.toSubsemiringClass` `Subring.instSubringClass` `IsLocalRing.of_surjective'` `Subring.instNontrivialSubtypeMem` `Set.mem_image_of_mem`
`isLocalRing_top` 📖	mathematical	—	`IsLocalRing` `Subring` `CommRing.toRing` `SetLike.instMembership` `Subring.instSetLike` `Top.top` `Subring.instTop` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `CommRing.toCommSemiring` `SubringClass.toSubsemiringClass` `Subring.instSubringClass`	—	`RingEquiv.isLocalRing` `SubringClass.toSubsemiringClass` `Subring.instSubringClass`

---

← Back to Index