Commit 2023-01-25 20:19 da1e6541

View on Github →

Refactor: use Option.map₂ (#1439) This is a forward-port of leanprover-community/mathlib#18081

Estimated changes

Modified Mathlib/Algebra/Group/WithOne/Defs.lean

deleted theorem WithZero.mul_zero

deleted theorem WithZero.zero_mul

Modified Mathlib/Algebra/Order/Monoid/WithTop.lean

Modified Mathlib/Algebra/Order/Ring/WithTop.lean

modified theorem WithBot.coe_mul

Modified Mathlib/Data/Option/NAry.lean

added theorem Option.map₂_left_identity

added theorem Option.map₂_right_identity

Modified Mathlib/Data/Set/NAry.lean

added theorem Set.image2_left_identity

added theorem Set.image2_right_identity

Modified Mathlib/Order/WithBot.lean