Commit 2022-12-07 03:37 ed38b3a0

View on Github →

feat: port Algebra.Order.Monoid.[TypeTags, Units] (#873) mathlib3 SHA: f1a2caaf51ef593799107fe9a8d5e411599f3996

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Monoid/TypeTags.lean

added theorem Additive.ofMul_le

added theorem Additive.ofMul_lt

added theorem Additive.toMul_le

added theorem Additive.toMul_lt

added theorem Multiplicative.ofAdd_le

added theorem Multiplicative.ofAdd_lt

added theorem Multiplicative.toAdd_le

added theorem Multiplicative.toAdd_lt

Created Mathlib/Algebra/Order/Monoid/Units.lean

added theorem Units.max_val

added theorem Units.min_val

added def Units.orderEmbeddingVal

added theorem Units.val_le_val

added theorem Units.val_lt_val