Commit 2026-04-01 19:38 4609a298

View on Github →

chore(Algebra/Order): generalise ordered algebra lemmas (#37040)

  • Generalise lemmas from ordered algebras to ordered modules + mixins

Estimated changes

modified theorem algebraMap_le_algebraMap
modified theorem algebraMap_lt_algebraMap
modified theorem algebraMap_mono
modified theorem algebraMap_nonneg
modified theorem algebraMap_pos
modified theorem algebraMap_strictMono
added theorem smul_one_mono
added theorem smul_one_strictMono