Documentation

Mathlib.FieldTheory.RatFunc.AsPolynomial

Generalities on the polynomial structure of rational functions #

Main definitions #

Polynomial structure: C, X, eval #

source
def RatFunc.C {K : Type u} [CommRing K] [IsDomain K] :
K →+* RatFunc K

RatFunc.C a is the constant rational function a.

Equations
Instances For
    source
    @[simp]
    theorem RatFunc.algebraMap_eq_C {K : Type u} [CommRing K] [IsDomain K] :
    algebraMap K (RatFunc K) = RatFunc.C
    source
    @[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
    source
    @[simp]
    theorem RatFunc.algebraMap_comp_C {K : Type u} [CommRing K] [IsDomain K] :
    (algebraMap (Polynomial K) (RatFunc K)).comp Polynomial.C = RatFunc.C
    source
    theorem RatFunc.smul_eq_C_mul {K : Type u} [CommRing K] [IsDomain K] (r : K) (x : RatFunc K) :
    r • x = RatFunc.C r * x
    source
    def RatFunc.X {K : Type u} [CommRing K] [IsDomain K] :
    RatFunc K

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

    Equations
    Instances For
      source
      @[simp]
      theorem RatFunc.algebraMap_X {K : Type u} [CommRing K] [IsDomain K] :
      (algebraMap (Polynomial K) (RatFunc K)) Polynomial.X = RatFunc.X
      source
      @[simp]
      theorem RatFunc.num_C {K : Type u} [Field K] (c : K) :
      (RatFunc.C c).num = Polynomial.C c
      source
      @[simp]
      theorem RatFunc.denom_C {K : Type u} [Field K] (c : K) :
      (RatFunc.C c).denom = 1
      source
      @[simp]
      theorem RatFunc.num_X {K : Type u} [Field K] :
      RatFunc.X.num = Polynomial.X
      source
      @[simp]
      theorem RatFunc.denom_X {K : Type u} [Field K] :
      RatFunc.X.denom = 1
      source
      theorem RatFunc.X_ne_zero {K : Type u} [Field K] :
      RatFunc.X ≠ 0
      source
      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
        source
        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
        source
        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
        source
        @[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
        source
        @[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
        source
        @[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
        source
        @[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
        source
        @[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) :
        RatFunc.eval f a ((algebraMap S (RatFunc K)) p) = Polynomial.eval₂ f a ((algebraMap S (Polynomial K)) p)
        source
        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.

        source
        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.