feat(data/polynomial): C_neg and C_sub (#561)

leanprover-community · Jan 5, 2019 · 87bf618 · 87bf618
1 parent 78d0ebf
commit 87bf618
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/data/polynomial.lean b/data/polynomial.lean
@@ -792,6 +792,10 @@ variable {α}
 
 instance C.is_ring_hom : is_ring_hom (@C α _ _) := by apply is_ring_hom.of_semiring
 
+@[simp] lemma C_neg : C (-a) = -C a := is_ring_hom.map_neg C
+
+@[simp] lemma C_sub : C (a - b) = C a - C b := is_ring_hom.map_sub C
+
 instance eval₂.is_ring_hom {β} [comm_ring β]
   (f : α → β) [is_ring_hom f] {x : β} : is_ring_hom (eval₂ f x) :=
 by apply is_ring_hom.of_semiring