mathlib3
957f64ee - feat(algebra/floor): When the floor is strictly positive (#9625)

Commit

4 years ago

feat(algebra/floor): When the floor is strictly positive (#9625) `⌊a⌋₊` and `⌊a⌋` are strictly positive iff `1 ≤ a`. We use this to slightly golf IMO 2013 P5.

Author

YaelDillies

Parents

bcd79a1f

mathlib3 957f64ee - feat(algebra/floor): When the floor is strictly positive (#9625)

mathlib3
957f64ee - feat(algebra/floor): When the floor is strictly positive (#9625)