mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

chore(Algebra/Order/Lemmas): remove useless lemmas, use `ZeroLEOneClass`

Open astrainfinita opened this issue 1 year ago • 0 comments

There are still some useless lemmas that were simply ported from Algebra.Order.Monoid.Lemmas, such as just chain an existing lemma with an assumption and lemmas whose assumptions imply 1 ≤ 0. This PR removes them.

Also, some lemmas have both assumptions like 1 < a 0 < a. This PR uses ZeroLEOneClass to remove redundant assumptions.

Ported from https://github.com/leanprover-community/mathlib/pull/16525 and https://github.com/leanprover-community/mathlib/pull/18158

Open in Gitpod

astrainfinita avatar Dec 23 '23 23:12 astrainfinita