Commit 2022-12-29 11:25 8f4222c5

View on Github →

feat: port Logic.Equiv.Nat (#1227) See discussion here

Estimated changes

Modified Mathlib.lean

Created Mathlib/Logic/Equiv/Nat.lean

added def Equiv.boolProdNatEquivNat

added def Equiv.intEquivNat

added def Equiv.natSumNatEquivNat

added theorem Equiv.natSumNatEquivNat_apply

added def Equiv.prodEquivOfEquivNat