Def Nat.discriminate
Modification history
2023-07-10 13:59
Mathlib/Init/Data/Nat/Lemmas.lean
feat: port Init.Data.Nat.Lemmas (#5782) …
Modified Nat.discriminateView on Github →2022-06-23 18:33
Mathlib/Init/Data/Nat/Lemmas.lean
chore: fix unused variables from linter (#289) …
Modified Nat.discriminateView on Github →