Commit 2024-09-10 14:11 dc471f0e

View on Github →

feat(RingTheory.LocalRing.ResidueField.Basic): add finite_of_finite (#15725)

Estimated changes