Def ArchimedeanClass.FiniteElement

Modification history

2026-03-26 18:37
Mathlib/Algebra/Order/Ring/StandardPart.lean
chore: avoid `unfold _; infer_instance` (#37129) …
Added ArchimedeanClass.FiniteElementView on Github →