mathlib
55534c4f - feat(data/nat/basic): recursion for set nat (#10273)

Commit
4 years ago
feat(data/nat/basic): recursion for set nat (#10273) Adding a special case of `nat.le_rec_on` where the predicate is membership of a subset.
Parents
Loading