Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-27 19:36 ebb53dc3

View on Github →

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

Estimated changes

Modified src/data/rat/defs.lean

added theorem rat.pnat_denom_one

added theorem rat.pnat_denom_zero