Def ArchimedeanClass.FiniteResidueField.ofArchimedean

Modification history

2026-02-17 23:08
Mathlib/Algebra/Order/Ring/StandardPart.lean
chore: bump toolchain to v4.29.0-rc1 (#35459)
Deleted ArchimedeanClass.FiniteResidueField.ofArchimedeanView on Github →
2025-12-17 10:18
Mathlib/Algebra/Order/Ring/StandardPart.lean
feat: standard part in non-Archimedean field (#29687) …
Added ArchimedeanClass.FiniteResidueField.ofArchimedeanView on Github →