Documentation

Mathlib.FieldTheory.RatFunc.AsPolynomial

Generalities on the polynomial structure of rational functions #

Main definitions #

Polynomial structure: C, X, eval #

def RatFunc.C {K : Type u} [CommRing K] [IsDomain K] :

RatFunc.C a is the constant rational function a.

Equations
Instances For
    @[simp]
    theorem RatFunc.algebraMap_eq_C {K : Type u} [CommRing K] [IsDomain K] :
    algebraMap K (RatFunc K) = RatFunc.C
    @[simp]
    theorem RatFunc.algebraMap_C {K : Type u} [CommRing K] [IsDomain K] (a : K) :
    (algebraMap (Polynomial K) (RatFunc K)) (Polynomial.C a) = RatFunc.C a
    @[simp]
    theorem RatFunc.algebraMap_comp_C {K : Type u} [CommRing K] [IsDomain K] :
    (algebraMap (Polynomial K) (RatFunc K)).comp Polynomial.C = RatFunc.C
    theorem RatFunc.smul_eq_C_mul {K : Type u} [CommRing K] [IsDomain K] (r : K) (x : RatFunc K) :
    r x = RatFunc.C r * x
    def RatFunc.X {K : Type u} [CommRing K] [IsDomain K] :

    RatFunc.X is the polynomial variable (aka indeterminate).

    Equations
    Instances For
      @[simp]
      theorem RatFunc.algebraMap_X {K : Type u} [CommRing K] [IsDomain K] :
      (algebraMap (Polynomial K) (RatFunc K)) Polynomial.X = RatFunc.X
      @[simp]
      theorem RatFunc.num_C {K : Type u} [Field K] (c : K) :
      (RatFunc.C c).num = Polynomial.C c
      @[simp]
      theorem RatFunc.denom_C {K : Type u} [Field K] (c : K) :
      (RatFunc.C c).denom = 1
      @[simp]
      theorem RatFunc.num_X {K : Type u} [Field K] :
      RatFunc.X.num = Polynomial.X
      @[simp]
      theorem RatFunc.denom_X {K : Type u} [Field K] :
      RatFunc.X.denom = 1
      theorem RatFunc.X_ne_zero {K : Type u} [Field K] :
      RatFunc.X 0
      def RatFunc.eval {K : Type u} [Field K] {L : Type u} [Field L] (f : K →+* L) (a : L) (p : RatFunc K) :
      L

      Evaluate a rational function p given a ring hom f from the scalar field to the target and a value x for the variable in the target.

      Fractions are reduced by clearing common denominators before evaluating: eval id 1 ((X^2 - 1) / (X - 1)) = eval id 1 (X + 1) = 2, not 0 / 0 = 0.

      Equations
      Instances For
        theorem RatFunc.eval_eq_zero_of_eval₂_denom_eq_zero {K : Type u} [Field K] {L : Type u} [Field L] {f : K →+* L} {a : L} {x : RatFunc K} (h : Polynomial.eval₂ f a x.denom = 0) :
        RatFunc.eval f a x = 0
        theorem RatFunc.eval₂_denom_ne_zero {K : Type u} [Field K] {L : Type u} [Field L] {f : K →+* L} {a : L} {x : RatFunc K} (h : RatFunc.eval f a x 0) :
        Polynomial.eval₂ f a x.denom 0
        @[simp]
        theorem RatFunc.eval_C {K : Type u} [Field K] {L : Type u} [Field L] (f : K →+* L) (a : L) {c : K} :
        RatFunc.eval f a (RatFunc.C c) = f c
        @[simp]
        theorem RatFunc.eval_X {K : Type u} [Field K] {L : Type u} [Field L] (f : K →+* L) (a : L) :
        RatFunc.eval f a RatFunc.X = a
        @[simp]
        theorem RatFunc.eval_zero {K : Type u} [Field K] {L : Type u} [Field L] (f : K →+* L) (a : L) :
        RatFunc.eval f a 0 = 0
        @[simp]
        theorem RatFunc.eval_one {K : Type u} [Field K] {L : Type u} [Field L] (f : K →+* L) (a : L) :
        RatFunc.eval f a 1 = 1
        @[simp]
        theorem RatFunc.eval_algebraMap {K : Type u} [Field K] {L : Type u} [Field L] (f : K →+* L) (a : L) {S : Type u_1} [CommSemiring S] [Algebra S (Polynomial K)] (p : S) :
        theorem RatFunc.eval_add {K : Type u} [Field K] {L : Type u} [Field L] (f : K →+* L) (a : L) {x : RatFunc K} {y : RatFunc K} (hx : Polynomial.eval₂ f a x.denom 0) (hy : Polynomial.eval₂ f a y.denom 0) :
        RatFunc.eval f a (x + y) = RatFunc.eval f a x + RatFunc.eval f a y

        eval is an additive homomorphism except when a denominator evaluates to 0.

        Counterexample: eval _ 1 (X / (X-1)) + eval _ 1 (-1 / (X-1)) = 0 ... ≠ 1 = eval _ 1 ((X-1) / (X-1)).

        See also RatFunc.eval₂_denom_ne_zero to make the hypotheses simpler but less general.

        theorem RatFunc.eval_mul {K : Type u} [Field K] {L : Type u} [Field L] (f : K →+* L) (a : L) {x : RatFunc K} {y : RatFunc K} (hx : Polynomial.eval₂ f a x.denom 0) (hy : Polynomial.eval₂ f a y.denom 0) :
        RatFunc.eval f a (x * y) = RatFunc.eval f a x * RatFunc.eval f a y

        eval is a multiplicative homomorphism except when a denominator evaluates to 0.

        Counterexample: eval _ 0 X * eval _ 0 (1/X) = 0 ≠ 1 = eval _ 0 1 = eval _ 0 (X * 1/X).

        See also RatFunc.eval₂_denom_ne_zero to make the hypotheses simpler but less general.

        This is the principal ideal generated by X in the ring of polynomials over a field K, regarded as an element of the height-one-spectrum.

        Equations
        Instances For
          @[simp]
          theorem Polynomial.idealX_span (K : Type u_1) [Field K] :
          (Polynomial.idealX K).asIdeal = Ideal.span {Polynomial.X}
          @[simp]
          theorem Polynomial.valuation_X_eq_neg_one (K : Type u_1) [Field K] :
          (Polynomial.idealX K).valuation RatFunc.X = (Multiplicative.ofAdd (-1))
          theorem Polynomial.valuation_of_mk (K : Type u_1) [Field K] (f : Polynomial K) {g : Polynomial K} (hg : g 0) :
          (Polynomial.idealX K).valuation (RatFunc.mk f g) = (Polynomial.idealX K).intValuation f / (Polynomial.idealX K).intValuation g
          @[simp]
          theorem RatFunc.WithZero.valued_def (K : Type u_1) [Field K] {x : RatFunc K} :
          Valued.v x = (Polynomial.idealX K).valuation x