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

Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
leanprover-community · Aug 27, 2022 · ebb53dc · ebb53dc
1 parent 6901db6
commit ebb53dc
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/data/rat/defs.lean b/src/data/rat/defs.lean
@@ -907,6 +907,10 @@ by rw [pnat_denom, mk_pnat_eq, num_denom]
 lemma pnat_denom_eq_iff_denom_eq {x : ℚ} {n : ℕ+} : x.pnat_denom = n ↔ x.denom = ↑n :=
 subtype.ext_iff
 
+@[simp] lemma pnat_denom_one : (1 : ℚ).pnat_denom = 1 := rfl
+
+@[simp] lemma pnat_denom_zero : (0 : ℚ).pnat_denom = 1 := rfl
+
 end pnat_denom
 
 end rat