Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-14 09:00 995b47e5

View on Github →

refactor(*): use option.map₂ (#18081) Relevant parts are forward-ported as leanprover-community/mathlib4#1439

Estimated changes

Modified src/algebra/continued_fractions/convergents_equiv.lean

Modified src/algebra/group/with_one/defs.lean

deleted theorem with_zero.mul_zero

deleted theorem with_zero.zero_mul

Modified src/algebra/monoid_algebra/grading.lean

Modified src/algebra/order/monoid/with_top.lean

Modified src/algebra/order/ring/with_top.lean

modified theorem with_top.mul_def

Modified src/data/finset/n_ary.lean

added theorem finset.image₂_left_identity

added theorem finset.image₂_right_identity

Modified src/data/option/n_ary.lean

added theorem option.map₂_left_identity

added theorem option.map₂_right_identity

modified theorem option.map₂_some_some

Modified src/data/seq/seq.lean

modified theorem seq.nth_zip_with

modified def seq.zip_with

deleted theorem seq.zip_with_nth_none'

deleted theorem seq.zip_with_nth_none

deleted theorem seq.zip_with_nth_some

Modified src/data/set/n_ary.lean

added theorem set.image2_left_identity

added theorem set.image2_right_identity

Modified src/order/filter/n_ary.lean

added theorem filter.map₂_left_identity

added theorem filter.map₂_right_identity

Modified src/order/filter/pointwise.lean

Modified src/order/with_bot.lean