floor): `0 < fract a ↔ a ≠ ⌊a⌋` (#18317)

Commit

2 years ago

feat(algebra/order/floor): `0 < fract a ↔ a ≠ ⌊a⌋` (#18317) This PR adds a lemma on the fractional part: ```lean lemma fract_pos : 0 < fract a ↔ a ≠ ⌊a⌋ ```

Author

MichaelStollBayreuth

Parents

8233a1cb

mathlib afdb4342 - feat(algebra/order/floor): `0 < fract a ↔ a ≠ ⌊a⌋` (#18317)

mathlib
afdb4342 - feat(algebra/order/floor): `0 < fract a ↔ a ≠ ⌊a⌋` (#18317)