chore(data/finsupp/basic): Remove finsupp.leval which duplicates finsupp.lapply (#4876)

Author: eric-wieser

src/algebra/big_operators/finsupp.lean

@@ -21,7 +21,7 @@ variables {α : Type u} {ι : Type v} {β : Type w} [add_comm_monoid β]
 variables {s : finset α} {f : α → (ι →₀ β)} (i : ι)
 
 theorem finset.sum_apply' : (∑ k in s, f k) i = ∑ k in s, f k i :=
-(s.sum_hom $ finsupp.eval_add_hom i).symm
+(s.sum_hom $ finsupp.apply_add_hom i).symm
 
 variables {γ : Type u₁} {δ : Type v₁} [add_comm_monoid δ]
 variables (g : ι →₀ β) (k : ι → β → γ → δ) (x : γ)

src/data/finsupp/basic.lean

@@ -5,7 +5,7 @@ Authors: Johannes Hölzl, Scott Morrison
 -/
 import algebra.group.pi
 import algebra.big_operators.order
-import algebra.module.linear_map
+import algebra.module.basic
 import data.fintype.card
 import data.finset.preimage
 import data.multiset.antidiagonal
@@ -638,14 +638,18 @@ instance : add_monoid (α →₀ M) :=
   zero_add  := assume ⟨s, f, hf⟩, ext $ assume a, zero_add _,
   add_zero  := assume ⟨s, f, hf⟩, ext $ assume a, add_zero _ }
 
-/-- `finsupp.single` as an `add_monoid_hom`. -/
+/-- `finsupp.single` as an `add_monoid_hom`.
+
+See `finsupp.lsingle` for the stronger version as a linear map.
+-/
 @[simps] def single_add_hom (a : α) : M →+ α →₀ M :=
 ⟨single a, single_zero, λ _ _, single_add⟩
 
-/-- Evaluation of a function `f : α →₀ M` at a point as an additive monoid homomorphism. -/
-def eval_add_hom (a : α) : (α →₀ M) →+ M := ⟨λ g, g a, zero_apply, λ _ _, add_apply⟩
+/-- Evaluation of a function `f : α →₀ M` at a point as an additive monoid homomorphism.
 
-@[simp] lemma eval_add_hom_apply (a : α) (g : α →₀ M) : eval_add_hom a g = g a := rfl
+See `finsupp.lapply` for the stronger version as a linear map. -/
+@[simps apply]
+def apply_add_hom (a : α) : (α →₀ M) →+ M := ⟨λ g, g a, zero_apply, λ _ _, add_apply⟩
 
 lemma single_add_erase (a : α) (f : α →₀ M) : single a (f a) + f.erase a = f :=
 ext $ λ a',
@@ -834,7 +838,7 @@ finset.subset.antisymm
 @[simp] lemma sum_apply [has_zero M] [add_comm_monoid N]
   {f : α →₀ M} {g : α → M → β →₀ N} {a₂ : β} :
   (f.sum g) a₂ = f.sum (λa₁ b, g a₁ b a₂) :=
-(eval_add_hom a₂ : (β →₀ N) →+ _).map_sum _ _
+(apply_add_hom a₂ : (β →₀ N) →+ _).map_sum _ _
 
 lemma support_sum [has_zero M] [add_comm_monoid N]
   {f : α →₀ M} {g : α → M → (β →₀ N)} :
@@ -1608,24 +1612,7 @@ instance [semiring R] [add_comm_monoid M] [semimodule R M] : semimodule R (α 
   zero_smul := λ x, ext $ λ _, zero_smul _ _,
   smul_zero := λ x, ext $ λ _, smul_zero _ }
 
-variables {α M} (R)
-
-/-- Evaluation at point as a linear map. This version assumes that the codomain is a semimodule
-over some semiring. See also `leval`. -/
-def leval' [semiring R] [add_comm_monoid M] [semimodule R M] (a : α) :
-  (α →₀ M) →ₗ[R] M :=
-⟨λ g, g a, λ _ _, add_apply, λ _ _, rfl⟩
-
-@[simp] lemma coe_leval' [semiring R] [add_comm_monoid M] [semimodule R M] (a : α) (g : α →₀ M) :
-  leval' R a g = g a :=
-rfl
-
-variable {R}
-
-/-- Evaluation at point as a linear map. This version assumes that the codomain is a semiring. -/
-def leval [semiring R] (a : α) : (α →₀ R) →ₗ[R] R := leval' R a
-
-@[simp] lemma coe_leval [semiring R] (a : α) (g : α →₀ R) : leval a g = g a := rfl
+variables {α M} {R}
 
 lemma support_smul {_ : semiring R} [add_comm_monoid M] [semimodule R M] {b : R} {g : α →₀ M} :
   (b • g).support ⊆ g.support :=

src/data/polynomial/coeff.lean

@@ -48,7 +48,7 @@ by { rw [mem_support_to_fun, not_not], refl, }
 variable (R)
 /-- The nth coefficient, as a linear map. -/
 def lcoeff (n : ℕ) : polynomial R →ₗ[R] R :=
-finsupp.leval n
+finsupp.lapply n
 variable {R}
 
 @[simp] lemma lcoeff_apply (n : ℕ) (f : polynomial R) : lcoeff R n f = coeff f n := rfl

src/linear_algebra/basis.lean

@@ -149,7 +149,7 @@ begin
   { to_fun := λ x, f x i,
     map_add' := λ _ _, by rw [hadd, pi.add_apply],
     map_smul' := λ _ _, by rw [hsmul, pi.smul_apply] },
-  show (finsupp.leval i).comp hv.repr x = f_i x,
+  show (finsupp.lapply i).comp hv.repr x = f_i x,
   congr' 1,
   refine hv.ext (λ j, _),
   show hv.repr (v j) i = f (v j) i,

src/linear_algebra/finsupp.lean

@@ -81,7 +81,7 @@ lhom_ext $ λ a, linear_map.congr_fun (h a)
 
 /-- Interpret `λ (f : α →₀ M), f a` as a linear map. -/
 def lapply (a : α) : (α →₀ M) →ₗ[R] M :=
-{ map_smul' := assume a b, rfl, ..finsupp.eval_add_hom a }
+{ map_smul' := assume a b, rfl, ..finsupp.apply_add_hom a }
 
 section lsubtype_domain
 variables (s : set α)