Commit 2022-11-23 13:44 dceff8bd

View on Github →

feat: Port Data/Option/NAry.lean (#656) Mathport pretty much got it right from the getgo, there is some things that can no longer be simp, but most importantly a defeq broke. Mathlib sha 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Option/NAry.lean

added theorem Option.map_map₂

added theorem Option.map_map₂_antidistrib

added theorem Option.map_map₂_antidistrib_left

added theorem Option.map_map₂_antidistrib_right

added theorem Option.map_map₂_distrib

added theorem Option.map_map₂_distrib_left

added theorem Option.map_map₂_distrib_right

added theorem Option.map_map₂_right_anticomm

added theorem Option.map_map₂_right_comm

added theorem Option.map_uncurry

added def Option.map₂

added theorem Option.map₂_assoc

added theorem Option.map₂_coe_coe

added theorem Option.map₂_coe_left

added theorem Option.map₂_coe_right

added theorem Option.map₂_comm

added theorem Option.map₂_curry

added theorem Option.map₂_def

added theorem Option.map₂_eq_none_iff

added theorem Option.map₂_left_comm

added theorem Option.map₂_map_left

added theorem Option.map₂_map_left_anticomm

added theorem Option.map₂_map_left_comm

added theorem Option.map₂_map_right

added theorem Option.map₂_none_left

added theorem Option.map₂_none_right

added theorem Option.map₂_right_comm

added theorem Option.map₂_some_some

added theorem Option.map₂_swap

added theorem Option.mem_map₂_iff