feat(ring_theory/algebra) define algebra over a commutative ring

leanprover-community · Dec 19, 2018 · de33c4e · de33c4e
1 parent 293ba83
commit de33c4e
Show file tree

Hide file tree

Showing 2 changed files with 510 additions and 0 deletions.
diff --git a/linear_algebra/multivariate_polynomial.lean b/linear_algebra/multivariate_polynomial.lean
@@ -302,10 +302,25 @@ instance : module α (mv_polynomial σ α) := finsupp.to_module _ α
 instance C.is_ring_hom : is_ring_hom (C : α → mv_polynomial σ α) :=
 by apply is_ring_hom.of_semiring
 
+variables (σ a a')
 lemma C_sub : (C (a - a') : mv_polynomial σ α) = C a - C a' := is_ring_hom.map_sub _
 
 @[simp] lemma C_neg : (C (-a) : mv_polynomial σ α) = -C a := is_ring_hom.map_neg _
 
+variables {σ} (p)
+theorem C_mul' : mv_polynomial.C a * p = a • p :=
+begin
+  apply finsupp.induction p,
+  { exact (mul_zero $ mv_polynomial.C a).trans (@smul_zero α (mv_polynomial σ α) _ _ _ a).symm },
+  intros p b f haf hb0 ih,
+  rw [mul_add, ih, @smul_add α (mv_polynomial σ α) _ _ _ a], congr' 1,
+  rw [finsupp.mul_def, finsupp.smul_single, mv_polynomial.C, mv_polynomial.monomial],
+  rw [finsupp.sum_single_index, finsupp.sum_single_index, zero_add, smul_eq_mul],
+  { rw [mul_zero, finsupp.single_zero] },
+  { rw finsupp.sum_single_index,
+    all_goals { rw [zero_mul, finsupp.single_zero] } }
+end
+
 section eval₂
 
 variables [decidable_eq β] [comm_ring β]