Theorem Algebra.isSeparable_residueField_iff

Modification history

2026-05-01 19:07
Mathlib/RingTheory/LocalRing/ResidueField/Instances.lean
refactor(Localization/AtPrime/Basic): add predicate for algebra instance on `Localization.AtPrime` (#38465) …
Modified Algebra.isSeparable_residueField_iffView on Github →
2025-08-18 23:10
Mathlib/RingTheory/LocalRing/ResidueField/Instances.lean
chore(RingTheory): Merge `Mathlib/RingTheory/LocalRing/ResidueField/Algebraic.lean` into `Instances.lean` (#26157) …
Modified Algebra.isSeparable_residueField_iffView on Github →
2025-06-19 11:54
Mathlib/RingTheory/LocalRing/ResidueField/Instances.lean
feat(RingTheory/DedekindDomain): a prime divides the different ideal iff it is ramified (#25936)
Added Algebra.isSeparable_residueField_iffView on Github →