Mathlib v3 is deprecated. Go to Mathlib v4

Theorem equiv.nat_sum_nat_equiv_nat_apply

Modification history

2022-07-19 15:47

src/logic/equiv/nat.lean

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

Added equiv.nat_sum_nat_equiv_nat_apply View on Github →