mathlib
ebb53dc3 - feat(data/rat/defs): add two lemmas for `pnat_denom` of 0 and 1 (#15864)

Commit
3 years ago
feat(data/rat/defs): add two lemmas for `pnat_denom` of 0 and 1 (#15864) Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
Author
Parents
Loading