FormalConjecturesForMathlib.Algebra.Polynomial.Algebra

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module


public import Mathlib.Algebra.Polynomial.Bivariate
public import Mathlib.RingTheory.Algebraic.Pi@[expose] public noncomputable section
              
                Algebra over the Ring of Polynomials
              
variable {R S : Type*} [CommSemiring R] [CommSemiring S] [Algebra R S]namespace Polynomialinstance instAlgebraPi : Algebra R[X] (S → S) :=
  (RingHom.pi fun s ↦ (Polynomial.aeval s).toRingHom).toAlgebra@[simp]
lemma algebraMap_algebraPi (p : R[X]) (s : S) : algebraMap R[X] (S → S) p s = aeval s p := rfl@[simp] lemma aeval_polynomial_pi (p : R[X][X]) (f : S → S) (x : S) :
    p.aeval f x = aevalAeval x (f x) p := byR:Type u_1S:Type u_2inst✝²:CommSemiring Rinst✝¹:CommSemiring Sinst✝:Algebra R Sp:R[X][X]f:S → Sx:S⊢ (aeval f) p x = (aevalAeval x (f x)) p
  induction p using Polynomial.induction_on' with
  | add =>addR:Type u_1S:Type u_2inst✝²:CommSemiring Rinst✝¹:CommSemiring Sinst✝:Algebra R Sf:S → Sx:Sp✝:R[X][X]q✝:R[X][X]a✝¹:(aeval f) p✝ x = (aevalAeval x (f x)) p✝a✝:(aeval f) q✝ x = (aevalAeval x (f x)) q✝⊢ (aeval f) (p✝ + q✝) x = (aevalAeval x (f x)) (p✝ + q✝) simp [*]All goals completed! 🐙
  | monomial n q =>monomialR:Type u_1S:Type u_2inst✝²:CommSemiring Rinst✝¹:CommSemiring Sinst✝:Algebra R Sf:S → Sx:Sn:ℕq:R[X]⊢ (aeval f) ((monomial n) q) x = (aevalAeval x (f x)) ((monomial n) q)
  simp only [aeval_monomial, Pi.mul_apply, Pi.pow_apply, aevalAevalEquiv_apply_apply,
    algebraMap_def, coe_mapRingHom, eval_mul, eval_map_algebraMap, eval_pow, eval_C]monomialR:Type u_1S:Type u_2inst✝²:CommSemiring Rinst✝¹:CommSemiring Sinst✝:Algebra R Sf:S → Sx:Sn:ℕq:R[X]⊢ (algebraMap R[X] (S → S)) q x * f x ^ n = (aeval x) q * f x ^ n
  induction q using Polynomial.induction_on' with
  | add =>monomial.addR:Type u_1S:Type u_2inst✝²:CommSemiring Rinst✝¹:CommSemiring Sinst✝:Algebra R Sf:S → Sx:Sn:ℕp✝:R[X]q✝:R[X]a✝¹:(algebraMap R[X] (S → S)) p✝ x * f x ^ n = (aeval x) p✝ * f x ^ na✝:(algebraMap R[X] (S → S)) q✝ x * f x ^ n = (aeval x) q✝ * f x ^ n⊢ (algebraMap R[X] (S → S)) (p✝ + q✝) x * f x ^ n = (aeval x) (p✝ + q✝) * f x ^ n simp [add_mul, *]All goals completed! 🐙
  | monomial n p =>monomial.monomialR:Type u_1S:Type u_2inst✝²:CommSemiring Rinst✝¹:CommSemiring Sinst✝:Algebra R Sf:S → Sx:Sn✝:ℕn:ℕp:R⊢ (algebraMap R[X] (S → S)) ((monomial n) p) x * f x ^ n✝ = (aeval x) ((monomial n) p) * f x ^ n✝ simpAll goals completed! 🐙end Polynomial