Theorem exists_floor

Modification history

2023-01-19 07:45

Mathlib/Algebra/Order/Archimedean.lean

chore: format `by` line breaks (#1523) …

Modified exists_floor View on Github →

2023-01-10 21:45

Mathlib/Algebra/Order/Archimedean.lean

feat: port Algebra.Order.Archimedean (#1462)

Added exists_floor View on Github →