Theorem ArchimedeanClass.FiniteResidueField.ordConnected_preimage_mk'

Modification history

2025-12-29 14:28
Mathlib/Algebra/Order/Ring/StandardPart.lean
feat: more lemmas on `ArchimedeanClass.stdPart` (#33343) …
Deleted ArchimedeanClass.FiniteResidueField.ordConnected_preimage_mk'View on Github →
2025-12-19 12:06
Mathlib/Algebra/Order/Ring/StandardPart.lean
chore: remove backward.privateInPublic from lakefile (#33034) …
Added ArchimedeanClass.FiniteResidueField.ordConnected_preimage_mk'View on Github →