Documentation

Mathlib.Algebra.Polynomial.Bivariate

Bivariate polynomials #

This file introduces the notation R[X][Y] for the polynomial ring R[X][X] in two variables, and the notation Y for the second variable, in the Polynomial scope.

It also defines Polynomial.evalEval for the evaluation of a bivariate polynomial at a point on the affine plane, which is a ring homomorphism (Polynomial.evalEvalRingHom), as well as the abbreviation CC to view a constant in the base ring R as a bivariate polynomial.

Pretty printer defined by notation3 command.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    The notation Y for X in the Polynomial scope.

    Equations
    Instances For

      Pretty printer defined by notation3 command.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        The notation R[X][Y] for R[X][X] in the Polynomial scope.

        Equations
        Instances For
          @[reducible, inline]
          abbrev Polynomial.evalEval {R : Type u_1} [Semiring R] (x : R) (y : R) (p : Polynomial (Polynomial R)) :
          R

          evalEval x y p is the evaluation p(x,y) of a two-variable polynomial p : R[X][Y].

          Equations
          Instances For
            @[reducible, inline]
            abbrev Polynomial.CC {R : Type u_1} [Semiring R] (r : R) :

            A constant viewed as a polynomial in two variables.

            Equations
            Instances For
              theorem Polynomial.evalEval_C {R : Type u_1} [Semiring R] (x : R) (y : R) (p : Polynomial R) :
              Polynomial.evalEval x y (Polynomial.C p) = Polynomial.eval x p
              @[simp]
              theorem Polynomial.evalEval_CC {R : Type u_1} [Semiring R] (x : R) (y : R) (p : R) :
              @[simp]
              theorem Polynomial.evalEval_zero {R : Type u_1} [Semiring R] (x : R) (y : R) :
              @[simp]
              theorem Polynomial.evalEval_one {R : Type u_1} [Semiring R] (x : R) (y : R) :
              @[simp]
              theorem Polynomial.evalEval_natCast {R : Type u_1} [Semiring R] (x : R) (y : R) (n : ) :
              Polynomial.evalEval x y n = n
              @[simp]
              theorem Polynomial.evalEval_X {R : Type u_1} [Semiring R] (x : R) (y : R) :
              Polynomial.evalEval x y Polynomial.X = y
              @[simp]
              theorem Polynomial.evalEval_add {R : Type u_1} [Semiring R] (x : R) (y : R) (p : Polynomial (Polynomial R)) (q : Polynomial (Polynomial R)) :
              theorem Polynomial.evalEval_sum {R : Type u_1} [Semiring R] (x : R) (y : R) (p : Polynomial R) (f : RPolynomial (Polynomial R)) :
              Polynomial.evalEval x y (p.sum f) = p.sum fun (n : ) (a : R) => Polynomial.evalEval x y (f n a)
              theorem Polynomial.evalEval_finset_sum {R : Type u_1} [Semiring R] {ι : Type u_3} (s : Finset ι) (x : R) (y : R) (f : ιPolynomial (Polynomial R)) :
              Polynomial.evalEval x y (∑ is, f i) = is, Polynomial.evalEval x y (f i)
              @[simp]
              theorem Polynomial.evalEval_smul {R : Type u_1} {S : Type u_2} [Semiring R] [Monoid S] [DistribMulAction S R] [IsScalarTower S R R] (x : R) (y : R) (s : S) (p : Polynomial (Polynomial R)) :
              @[simp]
              theorem Polynomial.evalEval_neg {R : Type u_1} [Ring R] (x : R) (y : R) (p : Polynomial (Polynomial R)) :
              @[simp]
              theorem Polynomial.evalEval_sub {R : Type u_1} [Ring R] (x : R) (y : R) (p : Polynomial (Polynomial R)) (q : Polynomial (Polynomial R)) :
              @[simp]
              theorem Polynomial.evalEval_intCast {R : Type u_1} [Ring R] (x : R) (y : R) (n : ) :
              Polynomial.evalEval x y n = n
              @[simp]
              theorem Polynomial.evalEval_mul {R : Type u_1} [CommSemiring R] (x : R) (y : R) (p : Polynomial (Polynomial R)) (q : Polynomial (Polynomial R)) :
              theorem Polynomial.evalEval_prod {R : Type u_1} [CommSemiring R] {ι : Type u_3} (s : Finset ι) (x : R) (y : R) (p : ιPolynomial (Polynomial R)) :
              Polynomial.evalEval x y (∏ js, p j) = js, Polynomial.evalEval x y (p j)
              theorem Polynomial.evalEval_list_prod {R : Type u_1} [CommSemiring R] (x : R) (y : R) (l : List (Polynomial (Polynomial R))) :
              @[simp]
              theorem Polynomial.evalEval_pow {R : Type u_1} [CommSemiring R] (x : R) (y : R) (p : Polynomial (Polynomial R)) (n : ) :
              theorem Polynomial.evalEval_dvd {R : Type u_1} [CommSemiring R] (x : R) (y : R) {p : Polynomial (Polynomial R)} {q : Polynomial (Polynomial R)} :
              theorem Polynomial.coe_algebraMap_eq_CC {R : Type u_1} [CommSemiring R] :
              (algebraMap R (Polynomial (Polynomial R))) = Polynomial.CC
              @[simp]
              theorem Polynomial.evalEvalRingHom_apply {R : Type u_1} [CommSemiring R] (x : R) (y : R) :
              @[reducible, inline]
              abbrev Polynomial.evalEvalRingHom {R : Type u_1} [CommSemiring R] (x : R) (y : R) :

              evalEval x y as a ring homomorphism.

              Equations
              Instances For
                theorem Polynomial.map_mapRingHom_evalEval {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (p : Polynomial (Polynomial R)) (x : R) (y : R) :

                Two equivalent ways to express the evaluation of a bivariate polynomial over R at a point in the affine plane over an R-algebra S.

                theorem Polynomial.eval_C_X_eval₂_map_C_X {R : Type u_1} [CommSemiring R] {p : Polynomial (Polynomial R)} :
                Polynomial.eval (Polynomial.C Polynomial.X) (Polynomial.eval₂ (Polynomial.mapRingHom (algebraMap R (Polynomial (Polynomial R)))) (Polynomial.C Polynomial.X) p) = p

                Viewing R[X,Y,X'] as an R[X']-algebra, a polynomial p : R[X',Y'] can be evaluated at Y : R[X,Y,X'] (substitution of Y' by Y), obtaining another polynomial in R[X,Y,X']. When this polynomial is then evaluated at X' = X, the original polynomial p is recovered.

                def AdjoinRoot.evalEval {R : Type u_1} [CommRing R] {x : R} {y : R} {p : Polynomial (Polynomial R)} (h : Polynomial.evalEval x y p = 0) :

                If the evaluation (evalEval) of a bivariate polynomial p : R[X][Y] at a point (x,y) is zero, then Polynomial.evalEval x y factors through AdjoinRoot.evalEval, a ring homomorphism from AdjoinRoot p to R.

                Equations
                Instances For
                  theorem AdjoinRoot.evalEval_mk {R : Type u_1} [CommRing R] {x : R} {y : R} {p : Polynomial (Polynomial R)} (h : Polynomial.evalEval x y p = 0) (g : Polynomial (Polynomial R)) :