Theorem IsLocalRing.ResidueField.finite_of_finite

Modification history

2025-02-04 14:13

Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean

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

Modified IsLocalRing.ResidueField.finite_of_finite View on Github →

2024-11-12 11:09

Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean

chore: rename `LocalRing` to `IsLocalRing` (#18774)

Added IsLocalRing.ResidueField.finite_of_finite View on Github →