Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-19 15:47 fd7796a1

View on Github →

chore(logic/equiv): improve defeq and/or simp lemmas about some equivs (#15511)

Estimated changes

Modified src/logic/equiv/basic.lean

modified def equiv.bool_prod_equiv_sum

Modified src/logic/equiv/nat.lean

modified def equiv.bool_prod_nat_equiv_nat

modified def equiv.nat_sum_nat_equiv_nat

added theorem equiv.nat_sum_nat_equiv_nat_apply