Algebraic functions

This file defines algebraic functions as the image of the algebraMap R[X] (R → S).

def Polynomial.hasSMulPi (R : Type u_1) (S : Type u_2) [Semiring R] [SMul R S] : SMul (Polynomial R) (R → S)

This is not an instance as it forms a diamond with Pi.instSMul.

See the instance_diamonds test for details.

noncomputable def Polynomial.hasSMulPi' (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommSemiring R] [Semiring S] [Algebra R S] [SMul S T] : SMul (Polynomial R) (S → T)

This is not an instance as it forms a diamond with Pi.instSMul.

See the instance_diamonds test for details.

@[simp]

theorem polynomial_smul_apply (R : Type u_1) (S : Type u_2) [Semiring R] [SMul R S] (p : Polynomial R) (f : R → S) (x : R) : (p • f) x = Polynomial.eval x p • f x

@[simp]

theorem polynomial_smul_apply' (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommSemiring R] [Semiring S] [Algebra R S] [SMul S T] (p : Polynomial R) (f : S → T) (x : S) : (p • f) x = (Polynomial.aeval x) p • f x

noncomputable def Polynomial.algebraPi (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommSemiring R] [CommSemiring S] [CommSemiring T] [Algebra R S] [Algebra S T] : Algebra (Polynomial R) (S → T)

This is not an instance for the same reasons as Polynomial.hasSMulPi'.

@[simp]

theorem Polynomial.algebraMap_pi_eq_aeval (R : Type u_1) (S : Type u_2) (T : Type u_3) [CommSemiring R] [CommSemiring S] [CommSemiring T] [Algebra R S] [Algebra S T] : ⇑(algebraMap (Polynomial R) (S → T)) = fun (p : Polynomial R) (z : S) => (algebraMap S T) ((aeval z) p)

@[simp]

theorem Polynomial.algebraMap_pi_self_eq_eval (R : Type u_1) [CommSemiring R] : ⇑(algebraMap (Polynomial R) (R → R)) = fun (p : Polynomial R) (z : R) => eval z p