Commit 2025-02-01 06:30 a8021cc6

View on Github →

feat(RingTheory/LocalRing): IsLocalRing for subrings (#21168) Results with some sufficient conditions for subrings of local rings to be local.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Ring/Subsemiring/Basic.lean

added theorem Subsemiring.inclusion_injective

Modified Mathlib/Algebra/Ring/Subsemiring/Defs.lean

added theorem Subsemiring.subtype_injective

Created Mathlib/RingTheory/LocalRing/LocalSubring.lean

added theorem LocalSubring.le_def

added theorem LocalSubring.le_ofPrime

added def LocalSubring.map

added def LocalSubring.ofPrime

added def LocalSubring.ofPrimeEquiv

added def LocalSubring.range

added theorem LocalSubring.toSubring_injective

added theorem LocalSubring.toSubring_mono

added structure LocalSubring

Modified Mathlib/RingTheory/LocalRing/Subring.lean

added theorem IsLocalRing.of_injective

added theorem IsLocalRing.of_subring'

added theorem IsLocalRing.of_subring

deleted theorem LocalSubring.le_def

deleted theorem LocalSubring.le_ofPrime

deleted def LocalSubring.map

deleted def LocalSubring.ofPrime

deleted def LocalSubring.ofPrimeEquiv

deleted def LocalSubring.range

deleted theorem LocalSubring.toSubring_injective

deleted theorem LocalSubring.toSubring_mono

deleted structure LocalSubring

Modified Mathlib/RingTheory/Valuation/LocalSubring.lean