Commit 2023-02-17 15:32 04818fdf

View on Github →

feat: a ≤ b / c → a * c ≤ b (#2027) Match https://github.com/leanprover-community/mathlib/pull/18367

Estimated changes