Commit 2025-08-18 23:10 495d7000
View on Github →chore(RingTheory): Merge Mathlib/RingTheory/LocalRing/ResidueField/Algebraic.lean into Instances.lean (#26157)
This was added a week ago by myself so I don't think a deprecation is needed
chore(RingTheory): Merge Mathlib/RingTheory/LocalRing/ResidueField/Algebraic.lean into Instances.lean (#26157)
This was added a week ago by myself so I don't think a deprecation is needed