Commit 2020-10-05 19:45 21158c43

View on Github →

lint(data/pnat): Docstrings and an unused argument in pnat.basic, pnat.factors (#4443) Adds docstrings Changes div_exact from having one unused input of type k | m to div_exact m k.

Estimated changes

Modified src/data/pnat/basic.lean

modified def pnat.div_exact

modified theorem pnat.mul_div_exact

Modified src/data/pnat/factors.lean