Commit 2023-04-29 16:26 3894e489

View on Github →

feat: a * b ≠ b ↔ a ≠ 1 (#3726) https://github.com/leanprover-community/mathlib/pull/18635

Estimated changes

deleted theorem div_two_lt_of_pos
deleted theorem half_le_self
added theorem half_le_self_iff
deleted theorem half_lt_self
added theorem half_lt_self_iff