mathlib
b0b0d5e3 - feat(tactic/positivity): Extensions for `nat` constructions (#16728)

Commit
3 years ago
feat(tactic/positivity): Extensions for `nat` constructions (#16728) Introduce the following `positivity` extensions: * `positivity_succ` * `positivity_factorial` * `positivity_asc_factorial`
Author
Parents
Loading