feat(data/mv_polynomial): add mv_polynomial.linear_map_ext (#10945)

leanprover-community · Dec 21, 2021 · 4aa7ac6 · 4aa7ac6
1 parent 8dafccc
commit 4aa7ac6
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/src/data/mv_polynomial/basic.lean b/src/data/mv_polynomial/basic.lean
@@ -364,6 +364,11 @@ begin
   case h_X : p i hp { exact S.mul_mem hp (algebra.subset_adjoin $ mem_range_self _) }
 end
 
+@[ext] lemma linear_map_ext {M : Type*} [add_comm_monoid M] [module R M]
+  {f g : mv_polynomial σ R →ₗ[R] M} (h : ∀ s, f ∘ₗ monomial s = g ∘ₗ monomial s) :
+  f = g :=
+finsupp.lhom_ext' h
+
 section support
 
 /--