Commit 2021-11-14 15:22 7dc33bf7

View on Github →

feat(data/nat/basic): Some nat.find lemmas (#10263) This proves nat.find_le and nat.find_add and renames the current nat.find_le to nat.find_mono.

Estimated changes

Modified src/data/nat/basic.lean

added theorem nat.find_add

modified theorem nat.find_le

added theorem nat.find_mono

Modified src/ring_theory/multiplicity.lean