Mathlib v3 is deprecated. Go to Mathlib v4

Def equiv.nat_prod_nat_equiv_nat

Modification history

2022-07-19 21:09
src/logic/equiv/nat.lean
refactor(logic/equiv/nat): remove `equiv.nat_prod_nat_equiv_nat` (#15509) …
Deleted equiv.nat_prod_nat_equiv_natView on Github →
2019-07-11 13:58
src/data/equiv/nat.lean
refactor(*): change priority of \simeq (#1210) …
Modified equiv.nat_prod_nat_equiv_natView on Github →
2018-06-30 23:04
data/equiv/basic.lean
refactor(data/equiv): reorganize data.equiv deps
Modified equiv.nat_prod_nat_equiv_natView on Github →
2017-09-19 02:55
data/equiv.lean
refactor(data/equiv,encodable): refactor/simplify proofs
Modified equiv.nat_prod_nat_equiv_natView on Github →
2017-09-08 18:07
data/equiv.lean
chore(data/equiv): using nat pairing
Added equiv.nat_prod_nat_equiv_natView on Github →