Mathlib Changelog
v4
Changelog
About
Github
Theorem
LocalRing.ResidueField.finite_of_finite
Modification history
2024-11-12 11:09
Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean
chore: rename `LocalRing` to `IsLocalRing` (#18774)
Deleted
LocalRing.ResidueField.finite_of_finite
View on Github →
2024-09-10 14:11
Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean
feat(RingTheory.LocalRing.ResidueField.Basic): add finite_of_finite (#15725)
Added
LocalRing.ResidueField.finite_of_finite
View on Github →