Commit 2024-11-17 16:39 acffbb9f

View on Github →

chore: deduplicate BddAbove.mul (#19161)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Group/Pointwise/Bounds.lean

Deleted Mathlib/Data/Set/Pointwise/BoundedMul.lean

deleted theorem Set.BddAbove.mul