diff --git a/src/data/rat/defs.lean b/src/data/rat/defs.lean
index 1f4b953429037..678af31d05455 100644
--- 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