Theorem ArchimedeanClass.FiniteResidueField.mk_ratCast

Modification history

2025-12-24 17:12
Mathlib/Algebra/Order/Ring/StandardPart.lean
feat: more theorems on `ArchimedeanClass.stdPart` (#33048)
Added ArchimedeanClass.FiniteResidueField.mk_ratCastView on Github →