Theorem ArchimedeanClass.FiniteResidueField.lt_of_mk_lt_mk

Modification history

2025-12-17 10:18
Mathlib/Algebra/Order/Ring/StandardPart.lean
feat: standard part in non-Archimedean field (#29687) …
Added ArchimedeanClass.FiniteResidueField.lt_of_mk_lt_mkView on Github →