feat(data/{mv_}polynomial): make args to aeval implicit (#3494)

Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>

src/data/mv_polynomial.lean

@@ -931,7 +931,7 @@ section aeval
 
 /-! ### The algebra of multivariate polynomials -/
 
-variables (R : Type u) (A : Type v) (f : σ → A)
+variables {R : Type u} {A : Type v} (f : σ → A)
 variables [comm_semiring R] [comm_semiring A] [algebra R A]
 
 /-- A map `σ → A` where `A` is an algebra over `R` generates an `R`-algebra homomorphism
@@ -940,14 +940,14 @@ def aeval : mv_polynomial σ R →ₐ[R] A :=
 { commutes' := λ r, eval₂_C _ _ _
   .. eval₂_hom (algebra_map R A) f }
 
-theorem aeval_def (p : mv_polynomial σ R) : aeval R A f p = eval₂ (algebra_map R A) f p := rfl
+theorem aeval_def (p : mv_polynomial σ R) : aeval f p = eval₂ (algebra_map R A) f p := rfl
 
-@[simp] lemma aeval_X (s : σ) : aeval R A f (X s) = f s := eval₂_X _ _ _
+@[simp] lemma aeval_X (s : σ) : aeval f (X s : mv_polynomial _ R) = f s := eval₂_X _ _ _
 
-@[simp] lemma aeval_C (r : R) : aeval R A f (C r) = algebra_map R A r := eval₂_C _ _ _
+@[simp] lemma aeval_C (r : R) : aeval f (C r) = algebra_map R A r := eval₂_C _ _ _
 
 theorem eval_unique (φ : mv_polynomial σ R →ₐ[R] A) :
-  φ = aeval R A (φ ∘ X) :=
+  φ = aeval (φ ∘ X) :=
 begin
   ext p,
   apply mv_polynomial.induction_on p,

src/data/polynomial/algebra_map.lean

@@ -138,8 +138,6 @@ end comm_semiring
 section aeval
 variables [comm_semiring R] {p : polynomial R}
 
-variables (R) (A)
-
 -- TODO this could be generalized: there's no need for `A` to be commutative,
 -- we just need that `x` is central.
 variables [comm_semiring A] [algebra R A]
@@ -154,11 +152,11 @@ def aeval : polynomial R →ₐ[R] A :=
 
 variables {R A}
 
-theorem aeval_def (p : polynomial R) : aeval R A x p = eval₂ (algebra_map R A) x p := rfl
+theorem aeval_def (p : polynomial R) : aeval x p = eval₂ (algebra_map R A) x p := rfl
 
-@[simp] lemma aeval_X : aeval R A x X = x := eval₂_X _ x
+@[simp] lemma aeval_X : aeval x (X : polynomial R) = x := eval₂_X _ x
 
-@[simp] lemma aeval_C (r : R) : aeval R A x (C r) = algebra_map R A r := eval₂_C _ x
+@[simp] lemma aeval_C (r : R) : aeval x (C r) = algebra_map R A r := eval₂_C _ x
 
 theorem eval_unique (φ : polynomial R →ₐ[R] A) (p) :
   φ p = eval₂ (algebra_map R A) (φ X) p :=
@@ -171,16 +169,17 @@ begin
     rw [pow_succ', ← mul_assoc, φ.map_mul, eval₂_mul (algebra_map R A), eval₂_X, ih] }
 end
 
-theorem aeval_alg_hom (f : A →ₐ[R] B) (x : A) : aeval R B (f x) = f.comp (aeval R A x) :=
-alg_hom.ext $ λ p, by rw [eval_unique (f.comp (aeval R A x)), alg_hom.comp_apply, aeval_X, aeval_def]
+theorem aeval_alg_hom (f : A →ₐ[R] B) (x : A) : aeval (f x) = f.comp (aeval x) :=
+alg_hom.ext $ λ p, by rw [eval_unique (f.comp (aeval x)), alg_hom.comp_apply, aeval_X, aeval_def]
 
-theorem aeval_alg_hom_apply (f : A →ₐ[R] B) (x : A) (p) : aeval R B (f x) p = f (aeval R A x p) :=
+theorem aeval_alg_hom_apply (f : A →ₐ[R] B) (x : A) (p : polynomial R) :
+  aeval (f x) p = f (aeval x p) :=
 alg_hom.ext_iff.1 (aeval_alg_hom f x) p
 
 @[simp] lemma coe_aeval_eq_eval (r : R) :
-  (aeval R R r : polynomial R → R) = eval r := rfl
+  (aeval r : polynomial R → R) = eval r := rfl
 
-lemma coeff_zero_eq_aeval_zero (p : polynomial R) : p.coeff 0 = aeval R R 0 p :=
+lemma coeff_zero_eq_aeval_zero (p : polynomial R) : p.coeff 0 = aeval 0 p :=
 by simp [coeff_zero_eq_eval_zero]
 
 lemma pow_comp (p q : polynomial R) (k : ℕ) : (p ^ k).comp q = (p.comp q) ^ k :=
@@ -198,7 +197,7 @@ end
 
 lemma is_root_of_aeval_algebra_map_eq_zero [algebra R S] {p : polynomial R}
   (inj : function.injective (algebra_map R S))
-  {r : R} (hr : aeval R S (algebra_map R S r) p = 0) : p.is_root r :=
+  {r : R} (hr : aeval (algebra_map R S r) p = 0) : p.is_root r :=
 is_root_of_eval₂_map_eq_zero inj hr
 
 lemma dvd_term_of_dvd_eval_of_dvd_terms {z p : S} {f : polynomial S} (i : ℕ)

src/data/polynomial/monic.lean

@@ -362,8 +362,8 @@ calc eval₂ f (z * f p.leading_coeff) (integral_normalization p)
 ... = 0 : by rw [hz, _root_.mul_zero]
 
 lemma integral_normalization_aeval_eq_zero [algebra R S] {f : polynomial R} (hf : f ≠ 0)
-  {z : S} (hz : aeval R S z f = 0) (inj : ∀ (x : R), algebra_map R S x = 0 → x = 0) :
-  aeval R S (z * algebra_map R S f.leading_coeff) (integral_normalization f) = 0 :=
+  {z : S} (hz : aeval z f = 0) (inj : ∀ (x : R), algebra_map R S x = 0 → x = 0) :
+  aeval (z * algebra_map R S f.leading_coeff) (integral_normalization f) = 0 :=
 integral_normalization_eval₂_eq_zero hf (algebra_map R S) hz inj
 end domain
 end integral_normalization

src/data/polynomial/ring_division.lean

@@ -30,12 +30,12 @@ variables [comm_ring R] {p q : polynomial R}
 variables [comm_ring S]
 
 lemma nat_degree_pos_of_aeval_root [algebra R S] {p : polynomial R} (hp : p ≠ 0)
-  {z : S} (hz : aeval R S z p = 0) (inj : ∀ (x : R), algebra_map R S x = 0 → x = 0) :
+  {z : S} (hz : aeval z p = 0) (inj : ∀ (x : R), algebra_map R S x = 0 → x = 0) :
   0 < p.nat_degree :=
 nat_degree_pos_of_eval₂_root hp (algebra_map R S) hz inj
 
 lemma degree_pos_of_aeval_root [algebra R S] {p : polynomial R} (hp : p ≠ 0)
-  {z : S} (hz : aeval R S z p = 0) (inj : ∀ (x : R), algebra_map R S x = 0 → x = 0) :
+  {z : S} (hz : aeval z p = 0) (inj : ∀ (x : R), algebra_map R S x = 0 → x = 0) :
   0 < p.degree :=
 nat_degree_pos_iff_degree_pos.mp (nat_degree_pos_of_aeval_root hp hz inj)
 

src/field_theory/minimal_polynomial.lean

@@ -46,12 +46,12 @@ lemma monic : monic (minimal_polynomial hx) :=
 (well_founded.min_mem degree_lt_wf _ hx).1
 
 /--An element is a root of its minimal polynomial.-/
-@[simp] lemma aeval : aeval α β x (minimal_polynomial hx) = 0 :=
+@[simp] lemma aeval : aeval x (minimal_polynomial hx) = 0 :=
 (well_founded.min_mem degree_lt_wf _ hx).2
 
 /--The defining property of the minimal polynomial of an element x:
 it is the monic polynomial with smallest degree that has x as its root.-/
-lemma min {p : polynomial α} (pmonic : p.monic) (hp : polynomial.aeval α β x p = 0) :
+lemma min {p : polynomial α} (pmonic : p.monic) (hp : polynomial.aeval x p = 0) :
   degree (minimal_polynomial hx) ≤ degree p :=
 le_of_not_lt $ well_founded.not_lt_min degree_lt_wf _ hx ⟨pmonic, hp⟩
 
@@ -68,7 +68,7 @@ ne_zero_of_monic (monic hx)
 /--If an element x is a root of a nonzero polynomial p,
 then the degree of p is at least the degree of the minimal polynomial of x.-/
 lemma degree_le_of_ne_zero
-  {p : polynomial α} (pnz : p ≠ 0) (hp : polynomial.aeval α β x p = 0) :
+  {p : polynomial α} (pnz : p ≠ 0) (hp : polynomial.aeval x p = 0) :
   degree (minimal_polynomial hx) ≤ degree p :=
 calc degree (minimal_polynomial hx) ≤ degree (p * C (leading_coeff p)⁻¹) :
     min _ (monic_mul_leading_coeff_inv pnz) (by simp [hp])
@@ -77,8 +77,8 @@ calc degree (minimal_polynomial hx) ≤ degree (p * C (leading_coeff p)⁻¹) :
 /--The minimal polynomial of an element x is uniquely characterized by its defining property:
 if there is another monic polynomial of minimal degree that has x as a root,
 then this polynomial is equal to the minimal polynomial of x.-/
-lemma unique {p : polynomial α} (pmonic : p.monic) (hp : polynomial.aeval α β x p = 0)
-  (pmin : ∀ q : polynomial α, q.monic → polynomial.aeval α β x q = 0 → degree p ≤ degree q) :
+lemma unique {p : polynomial α} (pmonic : p.monic) (hp : polynomial.aeval x p = 0)
+  (pmin : ∀ q : polynomial α, q.monic → polynomial.aeval x q = 0 → degree p ≤ degree q) :
   p = minimal_polynomial hx :=
 begin
   symmetry, apply eq_of_sub_eq_zero,
@@ -92,7 +92,7 @@ begin
 end
 
 /--If an element x is a root of a polynomial p, then the minimal polynomial of x divides p.-/
-lemma dvd {p : polynomial α} (hp : polynomial.aeval α β x p = 0) :
+lemma dvd {p : polynomial α} (hp : polynomial.aeval x p = 0) :
   minimal_polynomial hx ∣ p :=
 begin
   rw ← dvd_iff_mod_by_monic_eq_zero (monic hx),
@@ -129,8 +129,8 @@ lemma prime : prime (minimal_polynomial hx) :=
 begin
   refine ⟨ne_zero hx, not_is_unit hx, _⟩,
   rintros p q ⟨d, h⟩,
-  have :    polynomial.aeval α β x (p*q) = 0 := by simp [h, aeval hx],
-  replace : polynomial.aeval α β x p = 0 ∨ polynomial.aeval α β x q = 0 := by simpa,
+  have :    polynomial.aeval x (p*q) = 0 := by simp [h, aeval hx],
+  replace : polynomial.aeval x p = 0 ∨ polynomial.aeval x q = 0 := by simpa,
   cases this; [left, right]; apply dvd; assumption
 end
 

src/ring_theory/adjoin.lean

@@ -79,16 +79,16 @@ le_antisymm
     (set.subset.trans (set.subset_union_right _ _) subset_adjoin))
 
 theorem adjoin_eq_range :
-  adjoin R s = (mv_polynomial.aeval R A (coe : s → A)).range :=
+  adjoin R s = (mv_polynomial.aeval (coe : s → A)).range :=
 le_antisymm
   (adjoin_le $ λ x hx, ⟨mv_polynomial.X ⟨x, hx⟩, mv_polynomial.eval₂_X _ _ _⟩)
   (λ x ⟨p, hp⟩, hp ▸ mv_polynomial.induction_on p
     (λ r, by rw [mv_polynomial.aeval_def, mv_polynomial.eval₂_C]; exact (adjoin R s).2 r)
     (λ p q hp hq, by rw alg_hom.map_add; exact is_add_submonoid.add_mem hp hq)
-    (λ p ⟨n, hn⟩ hp, by rw [alg_hom.map_mul, mv_polynomial.aeval_def _ _ _ (mv_polynomial.X _),
+    (λ p ⟨n, hn⟩ hp, by rw [alg_hom.map_mul, mv_polynomial.aeval_def _ (mv_polynomial.X _),
       mv_polynomial.eval₂_X]; exact is_submonoid.mul_mem hp (subset_adjoin hn)))
 
-theorem adjoin_singleton_eq_range (x : A) : adjoin R {x} = (polynomial.aeval R A x).range :=
+theorem adjoin_singleton_eq_range (x : A) : adjoin R {x} = (polynomial.aeval x).range :=
 le_antisymm
   (adjoin_le $ set.singleton_subset_iff.2 ⟨polynomial.X, polynomial.eval₂_X _ _⟩)
   (λ y ⟨p, hp⟩, hp ▸ polynomial.induction_on p

src/ring_theory/adjoin_root.lean

@@ -84,7 +84,7 @@ quotient.sound' (mem_span_singleton.2 $ by simp)
 
 @[simp] lemma mk_X : mk f X = root f := rfl
 
-@[simp] lemma aeval_eq (p : polynomial R) : aeval R (adjoin_root f) (root f) p = mk f p :=
+@[simp] lemma aeval_eq (p : polynomial R) : aeval (root f) p = mk f p :=
 polynomial.induction_on p (λ x, by { rw aeval_C, refl })
   (λ p q ihp ihq, by rw [alg_hom.map_add, ring_hom.map_add, ihp, ihq])
   (λ n x ih, by { rw [alg_hom.map_mul, aeval_C, alg_hom.map_pow, aeval_X,

src/ring_theory/algebra_tower.lean

@@ -128,8 +128,8 @@ of_algebra_map_eq $ λ x, rfl
 instance polynomial : is_algebra_tower R A (polynomial B) :=
 of_algebra_map_eq $ λ x, congr_arg polynomial.C $ algebra_map_apply R A B x
 
-theorem aeval_apply (x : B) (p) : polynomial.aeval R B x p =
-  polynomial.aeval A B x (polynomial.map (algebra_map R A) p) :=
+theorem aeval_apply (x : B) (p : polynomial R) : polynomial.aeval x p =
+  polynomial.aeval x (polynomial.map (algebra_map R A) p) :=
 by rw [polynomial.aeval_def, polynomial.aeval_def, polynomial.eval₂_map, algebra_map_eq R A B]
 
 end comm_semiring

src/ring_theory/algebraic.lean

@@ -27,7 +27,7 @@ variables (R : Type u) {A : Type v} [comm_ring R] [comm_ring A] [algebra R A]
 
 /-- An element of an R-algebra is algebraic over R if it is the root of a nonzero polynomial. -/
 def is_algebraic (x : A) : Prop :=
-∃ p : polynomial R, p ≠ 0 ∧ aeval R A x p = 0
+∃ p : polynomial R, p ≠ 0 ∧ aeval x p = 0
 
 variables {R}
 

src/ring_theory/integral_closure.lean

@@ -21,7 +21,7 @@ variables [algebra R A] [algebra R B]
 /-- An element `x` of an algebra `A` over a commutative ring `R` is said to be *integral*,
 if it is a root of some monic polynomial `p : polynomial R`. -/
 def is_integral (x : A) : Prop :=
-∃ p : polynomial R, monic p ∧ aeval R A x p = 0
+∃ p : polynomial R, monic p ∧ aeval x p = 0
 
 variables {R}
 theorem is_integral_algebra_map {x : R} : is_integral R (algebra_map R A x) :=
@@ -89,7 +89,7 @@ set.finite.induction_on hfs (λ _, ⟨{1}, submodule.ext $ λ x,
 theorem is_integral_of_noetherian' (H : is_noetherian R A) (x : A) :
   is_integral R x :=
 begin
-  let leval : @linear_map R (polynomial R) A _ _ _ _ _ := (aeval R A x).to_linear_map,
+  let leval : @linear_map R (polynomial R) A _ _ _ _ _ := (aeval x).to_linear_map,
   let D : ℕ → submodule R A := λ n, (degree_le R n).map leval,
   let M := well_founded.min (is_noetherian_iff_well_founded.1 H)
     (set.range D) ⟨_, ⟨0, rfl⟩⟩,
@@ -239,7 +239,7 @@ variables {R} {A}
 
 lemma integral_closure.is_integral (x : integral_closure R A) : is_integral R x :=
 exists_imp_exists
-  (λ p, and.imp_right (λ hp, show aeval R (integral_closure R A) x p = 0,
+  (λ p, and.imp_right (λ hp, show aeval x p = 0,
     from subtype.ext (trans (p.hom_eval₂ _ (integral_closure R A).val.to_ring_hom x) hp)))
   x.2
 
@@ -283,7 +283,7 @@ variables {R : Type*} {A : Type*} {B : Type*}
 variables [comm_ring R] [comm_ring A] [comm_ring B]
 variables [algebra A B] [algebra R B]
 
-lemma is_integral_trans_aux (x : B) {p : polynomial A} (pmonic : monic p) (hp : aeval A B x p = 0) :
+lemma is_integral_trans_aux (x : B) {p : polynomial A} (pmonic : monic p) (hp : aeval x p = 0) :
   is_integral (adjoin R (↑(p.map $ algebra_map A B).frange : set B)) x :=
 begin
   generalize hS : (↑(p.map $ algebra_map A B).frange : set B) = S,

src/ring_theory/localization.lean

@@ -838,7 +838,7 @@ trans (eval₂_map f.to_map g x).symm (by rw [hb, eval₂_smul, hx, smul_zero])
 
 lemma integer_normalization_aeval_eq_zero [algebra R R'] [algebra f.codomain R']
   [is_algebra_tower R f.codomain R'] (p : polynomial f.codomain)
-  {x : R'} (hx : aeval _ _ x p = 0) : aeval _ R' x (integer_normalization p) = 0 :=
+  {x : R'} (hx : aeval x p = 0) : aeval x (integer_normalization p) = 0 :=
 by rw [aeval_def, is_algebra_tower.algebra_map_eq R f.codomain R', algebra_map_eq,
     integer_normalization_eval₂_eq_zero _ _ hx]
 

src/ring_theory/polynomial/rational_root.lean

@@ -114,8 +114,8 @@ calc (scale_roots p s).support.sum (λ i, f (coeff p i * s ^ (p.nat_degree - i))
 ... = 0 : by rw [hr, _root_.mul_zero]
 
 lemma scale_roots_aeval_eq_zero [algebra S R] {p : polynomial S}
-  {r : R} {s : S} (hr : aeval S R r p = 0) (hs : s ∈ non_zero_divisors S) :
-  aeval S R (algebra_map S R s * r) (scale_roots p s) = 0 :=
+  {r : R} {s : S} (hr : aeval r p = 0) (hs : s ∈ non_zero_divisors S) :
+  aeval (algebra_map S R s * r) (scale_roots p s) = 0 :=
 scale_roots_eval₂_eq_zero (algebra_map S R) hr hs
 
 lemma scale_roots_eval₂_eq_zero_of_eval₂_div_eq_zero
@@ -130,13 +130,13 @@ end
 
 lemma scale_roots_aeval_eq_zero_of_aeval_div_eq_zero [algebra A K]
   (inj : function.injective (algebra_map A K)) {p : polynomial A} {r s : A}
-  (hr : aeval A K (algebra_map A K r / algebra_map A K s) p = 0) (hs : s ∈ non_zero_divisors A) :
-  aeval A K (algebra_map A K r) (scale_roots p s) = 0 :=
+  (hr : aeval (algebra_map A K r / algebra_map A K s) p = 0) (hs : s ∈ non_zero_divisors A) :
+  aeval (algebra_map A K r) (scale_roots p s) = 0 :=
 scale_roots_eval₂_eq_zero_of_eval₂_div_eq_zero inj hr hs
 
 lemma scale_roots_aeval_eq_zero_of_aeval_mk'_eq_zero {p : polynomial A} {r : A} {s : M}
-  (hr : aeval A f.codomain (f.mk' r s) p = 0) (hM : M ≤ non_zero_divisors A) :
-  aeval A f.codomain (f.to_map r) (scale_roots p s) = 0 :=
+  (hr : @aeval A f.codomain _ _ _ (f.mk' r s) p = 0) (hM : M ≤ non_zero_divisors A) :
+  @aeval A f.codomain _ _ _ (f.to_map r) (scale_roots p s) = 0 :=
 begin
   convert scale_roots_eval₂_eq_zero f.to_map hr (hM s.2),
   rw aeval_def,
@@ -146,7 +146,7 @@ end
 
 lemma num_is_root_scale_roots_of_aeval_eq_zero
   [unique_factorization_domain A] (g : fraction_map A K)
-  {p : polynomial A} {x : g.codomain} (hr : aeval A g.codomain x p = 0) :
+  {p : polynomial A} {x : g.codomain} (hr : aeval x p = 0) :
   is_root (scale_roots p (g.denom x)) (g.num x) :=
 begin
   apply is_root_of_eval₂_map_eq_zero g.injective,
@@ -167,7 +167,7 @@ open polynomial unique_factorization_domain
 /-- Rational root theorem part 1:
 if `r : f.codomain` is a root of a polynomial over the ufd `A`,
 then the numerator of `r` divides the constant coefficient -/
-theorem num_dvd_of_is_root {p : polynomial A} {r} (hr : aeval A f.codomain r p = 0) :
+theorem num_dvd_of_is_root {p : polynomial A} {r : f.codomain} (hr : aeval r p = 0) :
   f.num r ∣ p.coeff 0 :=
 begin
   suffices : f.num r ∣ (scale_roots p (f.denom r)).coeff 0,
@@ -192,7 +192,7 @@ end
 /-- Rational root theorem part 2:
 if `r : f.codomain` is a root of a polynomial over the ufd `A`,
 then the denominator of `r` divides the leading coefficient -/
-theorem denom_dvd_of_is_root {p : polynomial A} {r} (hr : aeval A f.codomain r p = 0) :
+theorem denom_dvd_of_is_root {p : polynomial A} {r : f.codomain} (hr : aeval r p = 0) :
   (f.denom r : A) ∣ p.leading_coeff :=
 begin
   suffices : (f.denom r : A) ∣ p.leading_coeff * f.num r ^ p.nat_degree,
@@ -217,8 +217,8 @@ end
 /-- Integral root theorem:
 if `r : f.codomain` is a root of a monic polynomial over the ufd `A`,
 then `r` is an integer -/
-theorem is_integer_of_is_root_of_monic {p : polynomial A} (hp : monic p) {r}
-  (hr : aeval A f.codomain r p = 0) : f.is_integer r :=
+theorem is_integer_of_is_root_of_monic {p : polynomial A} (hp : monic p) {r : f.codomain}
+  (hr : aeval r p = 0) : f.is_integer r :=
 f.is_integer_of_is_unit_denom (is_unit_of_dvd_one _ (hp ▸ denom_dvd_of_is_root hr))
 
 namespace unique_factorization_domain