Commit 2025-02-04 14:13 cf27f6e9

View on Github →

feat(RingTheory): unramified iff κ(q)/κ(p) is separable and pS_q = qS_q (#20690)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/Artinian/Ring.lean

added theorem IsArtinianRing.isNilpotent_nilradical

added theorem IsArtinianRing.jacobson_eq_radical

Modified Mathlib/RingTheory/EssentialFiniteness.lean

Modified Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean

modified theorem IsLocalRing.ResidueField.finite_of_finite

Modified Mathlib/RingTheory/Unramified/Basic.lean

Modified Mathlib/RingTheory/Unramified/Field.lean

Created Mathlib/RingTheory/Unramified/LocalRing.lean

added theorem Algebra.FormallyUnramified.iff_map_maximalIdeal_eq

added theorem Algebra.FormallyUnramified.isField_quotient_map_maximalIdeal

added theorem Algebra.FormallyUnramified.map_maximalIdeal

added theorem Algebra.FormallyUnramified.of_map_maximalIdeal

added theorem Algebra.isUnramifiedAt_iff_map_eq

Modified Mathlib/RingTheory/Unramified/Locus.lean