Commit 2023-01-31 09:33 139af230

View on Github →

feat: port Data.W.Constructions (#1961)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/W/Constructions.lean

added inductive WType.Listα

added def WType.ListαEquivPUnitSum

added def WType.Listβ

added inductive WType.Natα

added def WType.NatαEquivPUnitSumPUnit

added def WType.Natβ

added def WType.equivList

added def WType.equivNat

added theorem WType.leftInverse_list

added theorem WType.leftInverse_nat

added def WType.ofList

added def WType.ofNat

added theorem WType.rightInverse_list

added theorem WType.rightInverse_nat

added def WType.toList

added def WType.toNat