Commit 2024-10-17 20:59 389e0979

View on Github →

chore(Algebra.Order.Monoid.TypeTags): split into unbundled and bundled ordered algebra (#16047) We move the unbundled ordered algebra results out of Algebra.Order.Monoid.TypeTags into Algebra.Order.Monoid.Unbundled.TypeTags to avoid importing bundled ordered algebra results unless necessary.

Estimated changes

deleted theorem Additive.ofMul_le
deleted theorem Additive.ofMul_lt
deleted theorem Additive.toMul_le
deleted theorem Additive.toMul_lt
deleted theorem Multiplicative.ofAdd_le
deleted theorem Multiplicative.ofAdd_lt
deleted theorem Multiplicative.toAdd_le
deleted theorem Multiplicative.toAdd_lt
added theorem Additive.ofMul_le
added theorem Additive.ofMul_lt
added theorem Additive.toMul_le
added theorem Additive.toMul_lt