Documentation

Mathlib.FieldTheory.RatFunc

The field of rational functions #

This file defines the field RatFunc K of rational functions over a field K, and shows it is the field of fractions of K[X].

Main definitions #

Working with rational functions as polynomials:

Working with rational functions as fractions:

Embedding of rational functions into Laurent series, provided as a coercion, utilizing the underlying RatFunc.coeAlgHom.

Lifting homomorphisms of polynomials to other types, by mapping and dividing, as long as the homomorphism retains the non-zero-divisor property:

We also have a set of recursion and induction principles:

We define the degree of a rational function, with values in :

Implementation notes #

To provide good API encapsulation and speed up unification problems, RatFunc is defined as a structure, and all operations are @[irreducible] defs

We need a couple of maps to set up the Field and IsFractionRing structure, namely RatFunc.ofFractionRing, RatFunc.toFractionRing, RatFunc.mk and RatFunc.toFractionRingRingEquiv. All these maps get simped to bundled morphisms like algebraMap K[X] (RatFunc K) and IsLocalization.algEquiv.

There are separate lifts and maps of homomorphisms, to provide routes of lifting even when the codomain is not a field or even an integral domain.

References #

structure RatFunc (K : Type u) [CommRing K] :

RatFunc K is K(X), the field of rational functions over K.

The inclusion of polynomials into RatFunc is algebraMap K[X] (RatFunc K), the maps between RatFunc K and another field of fractions of K[X], especially FractionRing K[X], are given by IsLocalization.algEquiv.

Instances For

    Constructing RatFuncs and their induction principles #

    theorem RatFunc.ofFractionRing_injective {K : Type u} [CommRing K] :
    Function.Injective RatFunc.ofFractionRing
    theorem RatFunc.toFractionRing_injective {K : Type u} [CommRing K] :
    Function.Injective RatFunc.toFractionRing
    theorem RatFunc.liftOn_def {K : Type u_1} [CommRing K] {P : Sort u_2} (x : RatFunc K) (f : Polynomial KPolynomial KP) (H : ∀ {p q p' q' : Polynomial K}, q nonZeroDivisors (Polynomial K)q' nonZeroDivisors (Polynomial K)q' * p = q * p'f p q = f p' q') :
    RatFunc.liftOn x f H = Localization.liftOn x.toFractionRing (fun (p : Polynomial K) (q : (nonZeroDivisors (Polynomial K))) => f p q)
    @[irreducible]
    def RatFunc.liftOn {K : Type u_1} [CommRing K] {P : Sort u_2} (x : RatFunc K) (f : Polynomial KPolynomial KP) (H : ∀ {p q p' q' : Polynomial K}, q nonZeroDivisors (Polynomial K)q' nonZeroDivisors (Polynomial K)q' * p = q * p'f p q = f p' q') :
    P

    Non-dependent recursion principle for RatFunc K: To construct a term of P : Sort* out of x : RatFunc K, it suffices to provide a constructor f : Π (p q : K[X]), P and a proof that f p q = f p' q' for all p q p' q' such that q' * p = q * p' where both q and q' are not zero divisors, stated as q ∉ K[X]⁰, q' ∉ K[X]⁰.

    If considering K as an integral domain, this is the same as saying that we construct a value of P for such elements of RatFunc K by setting liftOn (p / q) f _ = f p q.

    When [IsDomain K], one can use RatFunc.liftOn', which has the stronger requirement of ∀ {p q a : K[X]} (hq : q ≠ 0) (ha : a ≠ 0), f (a * p) (a * q) = f p q).

    Equations
    Instances For
      theorem RatFunc.liftOn_ofFractionRing_mk {K : Type u} [CommRing K] {P : Sort v} (n : Polynomial K) (d : (nonZeroDivisors (Polynomial K))) (f : Polynomial KPolynomial KP) (H : ∀ {p q p' q' : Polynomial K}, q nonZeroDivisors (Polynomial K)q' nonZeroDivisors (Polynomial K)q' * p = q * p'f p q = f p' q') :
      RatFunc.liftOn { toFractionRing := Localization.mk n d } f H = f n d
      theorem RatFunc.liftOn_condition_of_liftOn'_condition {K : Type u} [CommRing K] {P : Sort v} {f : Polynomial KPolynomial KP} (H : ∀ {p q a : Polynomial K}, q 0a 0f (a * p) (a * q) = f p q) ⦃p : Polynomial K ⦃q : Polynomial K ⦃p' : Polynomial K ⦃q' : Polynomial K (hq : q 0) (hq' : q' 0) (h : q' * p = q * p') :
      f p q = f p' q'
      @[irreducible]
      def RatFunc.mk {K : Type u_1} [CommRing K] [IsDomain K] (p : Polynomial K) (q : Polynomial K) :

      RatFunc.mk (p q : K[X]) is p / q as a rational function.

      If q = 0, then mk returns 0.

      This is an auxiliary definition used to define an Algebra structure on RatFunc; the simp normal form of mk p q is algebraMap _ _ p / algebraMap _ _ q.

      Equations
      Instances For
        theorem RatFunc.mk_def {K : Type u_1} [CommRing K] [IsDomain K] (p : Polynomial K) (q : Polynomial K) :
        RatFunc.mk p q = { toFractionRing := (algebraMap (Polynomial K) (FractionRing (Polynomial K))) p / (algebraMap (Polynomial K) (FractionRing (Polynomial K))) q }
        theorem RatFunc.mk_eq_div' {K : Type u} [CommRing K] [IsDomain K] (p : Polynomial K) (q : Polynomial K) :
        RatFunc.mk p q = { toFractionRing := (algebraMap (Polynomial K) (FractionRing (Polynomial K))) p / (algebraMap (Polynomial K) (FractionRing (Polynomial K))) q }
        theorem RatFunc.mk_zero {K : Type u} [CommRing K] [IsDomain K] (p : Polynomial K) :
        RatFunc.mk p 0 = { toFractionRing := 0 }
        theorem RatFunc.mk_coe_def {K : Type u} [CommRing K] [IsDomain K] (p : Polynomial K) (q : (nonZeroDivisors (Polynomial K))) :
        RatFunc.mk p q = { toFractionRing := IsLocalization.mk' (FractionRing (Polynomial K)) p q }
        theorem RatFunc.mk_def_of_mem {K : Type u} [CommRing K] [IsDomain K] (p : Polynomial K) {q : Polynomial K} (hq : q nonZeroDivisors (Polynomial K)) :
        RatFunc.mk p q = { toFractionRing := IsLocalization.mk' (FractionRing (Polynomial K)) p { val := q, property := hq } }
        theorem RatFunc.mk_def_of_ne {K : Type u} [CommRing K] [IsDomain K] (p : Polynomial K) {q : Polynomial K} (hq : q 0) :
        RatFunc.mk p q = { toFractionRing := IsLocalization.mk' (FractionRing (Polynomial K)) p { val := q, property := } }
        theorem RatFunc.mk_eq_localization_mk {K : Type u} [CommRing K] [IsDomain K] (p : Polynomial K) {q : Polynomial K} (hq : q 0) :
        RatFunc.mk p q = { toFractionRing := Localization.mk p { val := q, property := } }
        theorem RatFunc.mk_one' {K : Type u} [CommRing K] [IsDomain K] (p : Polynomial K) :
        RatFunc.mk p 1 = { toFractionRing := (algebraMap (Polynomial K) (FractionRing (Polynomial K))) p }
        theorem RatFunc.mk_eq_mk {K : Type u} [CommRing K] [IsDomain K] {p : Polynomial K} {q : Polynomial K} {p' : Polynomial K} {q' : Polynomial K} (hq : q 0) (hq' : q' 0) :
        RatFunc.mk p q = RatFunc.mk p' q' p * q' = p' * q
        theorem RatFunc.liftOn_mk {K : Type u} [CommRing K] [IsDomain K] {P : Sort v} (p : Polynomial K) (q : Polynomial K) (f : Polynomial KPolynomial KP) (f0 : ∀ (p : Polynomial K), f p 0 = f 0 1) (H' : ∀ {p q p' q' : Polynomial K}, q 0q' 0q' * p = q * p'f p q = f p' q') (H : optParam (∀ {p q p' q' : Polynomial K}, q nonZeroDivisors (Polynomial K)q' nonZeroDivisors (Polynomial K)q' * p = q * p'f p q = f p' q') ) :
        RatFunc.liftOn (RatFunc.mk p q) f H = f p q
        @[irreducible]
        def RatFunc.liftOn' {K : Type u_1} [CommRing K] [IsDomain K] {P : Sort u_2} (x : RatFunc K) (f : Polynomial KPolynomial KP) (H : ∀ {p q a : Polynomial K}, q 0a 0f (a * p) (a * q) = f p q) :
        P

        Non-dependent recursion principle for RatFunc K: if f p q : P for all p q, such that f (a * p) (a * q) = f p q, then we can find a value of P for all elements of RatFunc K by setting lift_on' (p / q) f _ = f p q.

        The value of f p 0 for any p is never used and in principle this may be anything, although many usages of lift_on' assume f p 0 = f 0 1.

        Equations
        Instances For
          theorem RatFunc.liftOn'_def {K : Type u_1} [CommRing K] [IsDomain K] {P : Sort u_2} (x : RatFunc K) (f : Polynomial KPolynomial KP) (H : ∀ {p q a : Polynomial K}, q 0a 0f (a * p) (a * q) = f p q) :
          theorem RatFunc.liftOn'_mk {K : Type u} [CommRing K] [IsDomain K] {P : Sort v} (p : Polynomial K) (q : Polynomial K) (f : Polynomial KPolynomial KP) (f0 : ∀ (p : Polynomial K), f p 0 = f 0 1) (H : ∀ {p q a : Polynomial K}, q 0a 0f (a * p) (a * q) = f p q) :
          RatFunc.liftOn' (RatFunc.mk p q) f H = f p q
          theorem RatFunc.induction_on' {K : Type u} [CommRing K] [IsDomain K] {P : RatFunc KProp} (x : RatFunc K) (_pq : ∀ (p q : Polynomial K), q 0P (RatFunc.mk p q)) :
          P x

          Induction principle for RatFunc K: if f p q : P (RatFunc.mk p q) for all p q, then P holds on all elements of RatFunc K.

          See also induction_on, which is a recursion principle defined in terms of algebraMap.

          Defining the field structure #

          @[irreducible]
          def RatFunc.zero {K : Type u_1} [CommRing K] :

          The zero rational function.

          Equations
          Instances For
            theorem RatFunc.zero_def {K : Type u_1} [CommRing K] :
            RatFunc.zero = { toFractionRing := 0 }
            Equations
            • RatFunc.instZeroRatFunc = { zero := RatFunc.zero }
            theorem RatFunc.ofFractionRing_zero {K : Type u} [CommRing K] :
            { toFractionRing := 0 } = 0
            theorem RatFunc.add_def {K : Type u_1} [CommRing K] :
            ∀ (x x_1 : RatFunc K), RatFunc.add x x_1 = match x, x_1 with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p + q }
            @[irreducible]
            def RatFunc.add {K : Type u_1} [CommRing K] :
            RatFunc KRatFunc KRatFunc K

            Addition of rational functions.

            Equations
            Instances For
              instance RatFunc.instAddRatFunc {K : Type u} [CommRing K] :
              Equations
              • RatFunc.instAddRatFunc = { add := RatFunc.add }
              theorem RatFunc.ofFractionRing_add {K : Type u} [CommRing K] (p : FractionRing (Polynomial K)) (q : FractionRing (Polynomial K)) :
              { toFractionRing := p + q } = { toFractionRing := p } + { toFractionRing := q }
              theorem RatFunc.sub_def {K : Type u_1} [CommRing K] :
              ∀ (x x_1 : RatFunc K), RatFunc.sub x x_1 = match x, x_1 with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p - q }
              @[irreducible]
              def RatFunc.sub {K : Type u_1} [CommRing K] :
              RatFunc KRatFunc KRatFunc K

              Subtraction of rational functions.

              Equations
              Instances For
                instance RatFunc.instSubRatFunc {K : Type u} [CommRing K] :
                Equations
                • RatFunc.instSubRatFunc = { sub := RatFunc.sub }
                theorem RatFunc.ofFractionRing_sub {K : Type u} [CommRing K] (p : FractionRing (Polynomial K)) (q : FractionRing (Polynomial K)) :
                { toFractionRing := p - q } = { toFractionRing := p } - { toFractionRing := q }
                theorem RatFunc.neg_def {K : Type u_1} [CommRing K] :
                ∀ (x : RatFunc K), RatFunc.neg x = match x with | { toFractionRing := p } => { toFractionRing := -p }
                @[irreducible]
                def RatFunc.neg {K : Type u_1} [CommRing K] :

                Additive inverse of a rational function.

                Equations
                Instances For
                  instance RatFunc.instNegRatFunc {K : Type u} [CommRing K] :
                  Equations
                  • RatFunc.instNegRatFunc = { neg := RatFunc.neg }
                  theorem RatFunc.ofFractionRing_neg {K : Type u} [CommRing K] (p : FractionRing (Polynomial K)) :
                  { toFractionRing := -p } = -{ toFractionRing := p }
                  theorem RatFunc.one_def {K : Type u_1} [CommRing K] :
                  RatFunc.one = { toFractionRing := 1 }
                  @[irreducible]
                  def RatFunc.one {K : Type u_1} [CommRing K] :

                  The multiplicative unit of rational functions.

                  Equations
                  Instances For
                    instance RatFunc.instOneRatFunc {K : Type u} [CommRing K] :
                    Equations
                    • RatFunc.instOneRatFunc = { one := RatFunc.one }
                    theorem RatFunc.ofFractionRing_one {K : Type u} [CommRing K] :
                    { toFractionRing := 1 } = 1
                    @[irreducible]
                    def RatFunc.mul {K : Type u_1} [CommRing K] :
                    RatFunc KRatFunc KRatFunc K

                    Multiplication of rational functions.

                    Equations
                    Instances For
                      theorem RatFunc.mul_def {K : Type u_1} [CommRing K] :
                      ∀ (x x_1 : RatFunc K), RatFunc.mul x x_1 = match x, x_1 with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p * q }
                      instance RatFunc.instMulRatFunc {K : Type u} [CommRing K] :
                      Equations
                      • RatFunc.instMulRatFunc = { mul := RatFunc.mul }
                      theorem RatFunc.ofFractionRing_mul {K : Type u} [CommRing K] (p : FractionRing (Polynomial K)) (q : FractionRing (Polynomial K)) :
                      { toFractionRing := p * q } = { toFractionRing := p } * { toFractionRing := q }
                      theorem RatFunc.div_def {K : Type u_1} [CommRing K] [IsDomain K] :
                      ∀ (x x_1 : RatFunc K), RatFunc.div x x_1 = match x, x_1 with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p / q }
                      @[irreducible]
                      def RatFunc.div {K : Type u_1} [CommRing K] [IsDomain K] :
                      RatFunc KRatFunc KRatFunc K

                      Division of rational functions.

                      Equations
                      Instances For
                        instance RatFunc.instDivRatFunc {K : Type u} [CommRing K] [IsDomain K] :
                        Equations
                        • RatFunc.instDivRatFunc = { div := RatFunc.div }
                        theorem RatFunc.ofFractionRing_div {K : Type u} [CommRing K] [IsDomain K] (p : FractionRing (Polynomial K)) (q : FractionRing (Polynomial K)) :
                        { toFractionRing := p / q } = { toFractionRing := p } / { toFractionRing := q }
                        @[irreducible]
                        def RatFunc.inv {K : Type u_1} [CommRing K] [IsDomain K] :

                        Multiplicative inverse of a rational function.

                        Equations
                        Instances For
                          theorem RatFunc.inv_def {K : Type u_1} [CommRing K] [IsDomain K] :
                          ∀ (x : RatFunc K), RatFunc.inv x = match x with | { toFractionRing := p } => { toFractionRing := p⁻¹ }
                          instance RatFunc.instInvRatFunc {K : Type u} [CommRing K] [IsDomain K] :
                          Equations
                          • RatFunc.instInvRatFunc = { inv := RatFunc.inv }
                          theorem RatFunc.ofFractionRing_inv {K : Type u} [CommRing K] [IsDomain K] (p : FractionRing (Polynomial K)) :
                          { toFractionRing := p⁻¹ } = { toFractionRing := p }⁻¹
                          theorem RatFunc.mul_inv_cancel {K : Type u} [CommRing K] [IsDomain K] {p : RatFunc K} :
                          p 0p * p⁻¹ = 1
                          theorem RatFunc.smul_def {K : Type u_2} [CommRing K] {R : Type u_3} [SMul R (FractionRing (Polynomial K))] :
                          ∀ (x : R) (x_1 : RatFunc K), RatFunc.smul x x_1 = match x, x_1 with | r, { toFractionRing := p } => { toFractionRing := r p }
                          @[irreducible]
                          def RatFunc.smul {K : Type u_2} [CommRing K] {R : Type u_3} [SMul R (FractionRing (Polynomial K))] :
                          RRatFunc KRatFunc K

                          Scalar multiplication of rational functions.

                          Equations
                          Instances For
                            instance RatFunc.instSMulRatFunc {K : Type u} [CommRing K] {R : Type u_1} [SMul R (FractionRing (Polynomial K))] :
                            Equations
                            • RatFunc.instSMulRatFunc = { smul := RatFunc.smul }
                            theorem RatFunc.ofFractionRing_smul {K : Type u} [CommRing K] {R : Type u_1} [SMul R (FractionRing (Polynomial K))] (c : R) (p : FractionRing (Polynomial K)) :
                            { toFractionRing := c p } = c { toFractionRing := p }
                            theorem RatFunc.toFractionRing_smul {K : Type u} [CommRing K] {R : Type u_1} [SMul R (FractionRing (Polynomial K))] (c : R) (p : RatFunc K) :
                            (c p).toFractionRing = c p.toFractionRing
                            theorem RatFunc.smul_eq_C_smul {K : Type u} [CommRing K] (x : RatFunc K) (r : K) :
                            r x = Polynomial.C r x
                            theorem RatFunc.mk_smul {K : Type u} [CommRing K] {R : Type u_1} [IsDomain K] [Monoid R] [DistribMulAction R (Polynomial K)] [IsScalarTower R (Polynomial K) (Polynomial K)] (c : R) (p : Polynomial K) (q : Polynomial K) :
                            RatFunc.mk (c p) q = c RatFunc.mk p q
                            Equations
                            • =
                            @[simp]
                            theorem RatFunc.toFractionRingRingEquiv_apply (K : Type u) [CommRing K] (self : RatFunc K) :
                            (RatFunc.toFractionRingRingEquiv K) self = self.toFractionRing

                            RatFunc K is isomorphic to the field of fractions of K[X], as rings.

                            This is an auxiliary definition; simp-normal form is IsLocalization.algEquiv.

                            Equations
                            • RatFunc.toFractionRingRingEquiv K = { toEquiv := { toFun := RatFunc.toFractionRing, invFun := RatFunc.ofFractionRing, left_inv := , right_inv := }, map_mul' := , map_add' := }
                            Instances For

                              Solve equations for RatFunc K by working in FractionRing K[X].

                              Equations
                              Instances For

                                Solve equations for RatFunc K by applying RatFunc.induction_on.

                                Equations
                                Instances For

                                  RatFunc K is a commutative monoid.

                                  This is an intermediate step on the way to the full instance RatFunc.instCommRing.

                                  Equations
                                  Instances For

                                    RatFunc K is an additive commutative group.

                                    This is an intermediate step on the way to the full instance RatFunc.instCommRing.

                                    Equations
                                    Instances For

                                      Lift a monoid homomorphism that maps polynomials φ : R[X] →* S[X] to a RatFunc R →* RatFunc S, on the condition that φ maps non zero divisors to non zero divisors, by mapping both the numerator and denominator and quotienting them.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        theorem RatFunc.map_apply_ofFractionRing_mk {R : Type u_3} {S : Type u_4} {F : Type u_5} [CommRing R] [CommRing S] [FunLike F (Polynomial R) (Polynomial S)] [MonoidHomClass F (Polynomial R) (Polynomial S)] (φ : F) (hφ : nonZeroDivisors (Polynomial R) Submonoid.comap φ (nonZeroDivisors (Polynomial S))) (n : Polynomial R) (d : (nonZeroDivisors (Polynomial R))) :
                                        (RatFunc.map φ ) { toFractionRing := Localization.mk n d } = { toFractionRing := Localization.mk (φ n) { val := φ d, property := } }

                                        Lift a ring homomorphism that maps polynomials φ : R[X] →+* S[X] to a RatFunc R →+* RatFunc S, on the condition that φ maps non zero divisors to non zero divisors, by mapping both the numerator and denominator and quotienting them.

                                        Equations
                                        Instances For

                                          Lift a monoid with zero homomorphism R[X] →*₀ G₀ to a RatFunc R →*₀ G₀ on the condition that φ maps non zero divisors to non zero divisors, by mapping both the numerator and denominator and quotienting them.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            theorem RatFunc.liftMonoidWithZeroHom_apply_ofFractionRing_mk {G₀ : Type u_1} {R : Type u_3} [CommGroupWithZero G₀] [CommRing R] (φ : Polynomial R →*₀ G₀) (hφ : nonZeroDivisors (Polynomial R) Submonoid.comap φ (nonZeroDivisors G₀)) (n : Polynomial R) (d : (nonZeroDivisors (Polynomial R))) :
                                            (RatFunc.liftMonoidWithZeroHom φ ) { toFractionRing := Localization.mk n d } = φ n / φ d

                                            Lift an injective ring homomorphism R[X] →+* L to a RatFunc R →+* L by mapping both the numerator and denominator and quotienting them.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              theorem RatFunc.liftRingHom_apply_ofFractionRing_mk {L : Type u_2} {R : Type u_3} [Field L] [CommRing R] (φ : Polynomial R →+* L) (hφ : nonZeroDivisors (Polynomial R) Submonoid.comap φ (nonZeroDivisors L)) (n : Polynomial R) (d : (nonZeroDivisors (Polynomial R))) :
                                              (RatFunc.liftRingHom φ ) { toFractionRing := Localization.mk n d } = φ n / φ d
                                              instance RatFunc.instField (K : Type u) [CommRing K] [IsDomain K] :
                                              Equations

                                              RatFunc as field of fractions of Polynomial #

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              theorem RatFunc.ofFractionRing_algebraMap {K : Type u} [CommRing K] [IsDomain K] (x : Polynomial K) :
                                              { toFractionRing := (algebraMap (Polynomial K) (FractionRing (Polynomial K))) x } = (algebraMap (Polynomial K) (RatFunc K)) x
                                              @[simp]
                                              theorem RatFunc.mk_eq_div {K : Type u} [CommRing K] [IsDomain K] (p : Polynomial K) (q : Polynomial K) :
                                              @[simp]
                                              theorem RatFunc.div_smul {K : Type u} [CommRing K] [IsDomain K] {R : Type u_1} [Monoid R] [DistribMulAction R (Polynomial K)] [IsScalarTower R (Polynomial K) (Polynomial K)] (c : R) (p : Polynomial K) (q : Polynomial K) :
                                              theorem RatFunc.algebraMap_apply {K : Type u} [CommRing K] [IsDomain K] {R : Type u_1} [CommSemiring R] [Algebra R (Polynomial K)] (x : R) :
                                              theorem RatFunc.map_apply_div_ne_zero {K : Type u} [CommRing K] [IsDomain K] {R : Type u_1} {F : Type u_2} [CommRing R] [IsDomain R] [FunLike F (Polynomial K) (Polynomial R)] [MonoidHomClass F (Polynomial K) (Polynomial R)] (φ : F) (hφ : nonZeroDivisors (Polynomial K) Submonoid.comap φ (nonZeroDivisors (Polynomial R))) (p : Polynomial K) (q : Polynomial K) (hq : q 0) :
                                              (RatFunc.map φ ) ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) = (algebraMap (Polynomial R) (RatFunc R)) (φ p) / (algebraMap (Polynomial R) (RatFunc R)) (φ q)
                                              @[simp]
                                              @[simp]
                                              theorem RatFunc.liftRingHom_apply_div' {K : Type u} [CommRing K] [IsDomain K] {L : Type u_1} [Field L] (φ : Polynomial K →+* L) (hφ : nonZeroDivisors (Polynomial K) Submonoid.comap φ (nonZeroDivisors L)) (p : Polynomial K) (q : Polynomial K) :
                                              (RatFunc.liftRingHom φ ) ((algebraMap (Polynomial K) (RatFunc K)) p) / (RatFunc.liftRingHom φ ) ((algebraMap (Polynomial K) (RatFunc K)) q) = φ p / φ q
                                              @[simp]
                                              theorem RatFunc.algebraMap_ne_zero {K : Type u} [CommRing K] [IsDomain K] {x : Polynomial K} (hx : x 0) :

                                              Lift an algebra homomorphism that maps polynomials φ : K[X] →ₐ[S] R[X] to a RatFunc K →ₐ[S] RatFunc R, on the condition that φ maps non zero divisors to non zero divisors, by mapping both the numerator and denominator and quotienting them.

                                              Equations
                                              Instances For

                                                Lift an injective algebra homomorphism K[X] →ₐ[S] L to a RatFunc K →ₐ[S] L by mapping both the numerator and denominator and quotienting them.

                                                Equations
                                                Instances For
                                                  theorem RatFunc.liftAlgHom_apply_ofFractionRing_mk {K : Type u} [CommRing K] [IsDomain K] {L : Type u_1} {S : Type u_3} [Field L] [CommSemiring S] [Algebra S (Polynomial K)] [Algebra S L] (φ : Polynomial K →ₐ[S] L) (hφ : nonZeroDivisors (Polynomial K) Submonoid.comap φ (nonZeroDivisors L)) (n : Polynomial K) (d : (nonZeroDivisors (Polynomial K))) :
                                                  (RatFunc.liftAlgHom φ ) { toFractionRing := Localization.mk n d } = φ n / φ d
                                                  @[simp]
                                                  theorem RatFunc.liftAlgHom_apply_div' {K : Type u} [CommRing K] [IsDomain K] {L : Type u_1} {S : Type u_3} [Field L] [CommSemiring S] [Algebra S (Polynomial K)] [Algebra S L] (φ : Polynomial K →ₐ[S] L) (hφ : nonZeroDivisors (Polynomial K) Submonoid.comap φ (nonZeroDivisors L)) (p : Polynomial K) (q : Polynomial K) :
                                                  (RatFunc.liftAlgHom φ ) ((algebraMap (Polynomial K) (RatFunc K)) p) / (RatFunc.liftAlgHom φ ) ((algebraMap (Polynomial K) (RatFunc K)) q) = φ p / φ q
                                                  theorem RatFunc.liftAlgHom_apply_div {K : Type u} [CommRing K] [IsDomain K] {L : Type u_1} {S : Type u_3} [Field L] [CommSemiring S] [Algebra S (Polynomial K)] [Algebra S L] (φ : Polynomial K →ₐ[S] L) (hφ : nonZeroDivisors (Polynomial K) Submonoid.comap φ (nonZeroDivisors L)) (p : Polynomial K) (q : Polynomial K) :
                                                  (RatFunc.liftAlgHom φ ) ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) = φ p / φ q
                                                  @[simp]
                                                  theorem RatFunc.liftOn_div {K : Type u} [CommRing K] [IsDomain K] {P : Sort v} (p : Polynomial K) (q : Polynomial K) (f : Polynomial KPolynomial KP) (f0 : ∀ (p : Polynomial K), f p 0 = f 0 1) (H' : ∀ {p q p' q' : Polynomial K}, q 0q' 0q' * p = q * p'f p q = f p' q') (H : optParam (∀ {p q p' q' : Polynomial K}, q nonZeroDivisors (Polynomial K)q' nonZeroDivisors (Polynomial K)q' * p = q * p'f p q = f p' q') ) :
                                                  @[simp]
                                                  theorem RatFunc.liftOn'_div {K : Type u} [CommRing K] [IsDomain K] {P : Sort v} (p : Polynomial K) (q : Polynomial K) (f : Polynomial KPolynomial KP) (f0 : ∀ (p : Polynomial K), f p 0 = f 0 1) (H : ∀ {p q a : Polynomial K}, q 0a 0f (a * p) (a * q) = f p q) :
                                                  theorem RatFunc.induction_on {K : Type u} [CommRing K] [IsDomain K] {P : RatFunc KProp} (x : RatFunc K) (f : ∀ (p q : Polynomial K), q 0P ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q)) :
                                                  P x

                                                  Induction principle for RatFunc K: if f p q : P (p / q) for all p q : K[X], then P holds on all elements of RatFunc K.

                                                  See also induction_on', which is a recursion principle defined in terms of RatFunc.mk.

                                                  @[simp]
                                                  @[simp]

                                                  Numerator and denominator #

                                                  RatFunc.numDenom are numerator and denominator of a rational function over a field, normalized such that the denominator is monic.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    @[simp]
                                                    theorem RatFunc.numDenom_div {K : Type u} [Field K] (p : Polynomial K) {q : Polynomial K} (hq : q 0) :
                                                    RatFunc.numDenom ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) = (Polynomial.C (Polynomial.leadingCoeff (q / gcd p q))⁻¹ * (p / gcd p q), Polynomial.C (Polynomial.leadingCoeff (q / gcd p q))⁻¹ * (q / gcd p q))
                                                    def RatFunc.num {K : Type u} [Field K] (x : RatFunc K) :

                                                    RatFunc.num is the numerator of a rational function, normalized such that the denominator is monic.

                                                    Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem RatFunc.num_zero {K : Type u} [Field K] :
                                                      @[simp]
                                                      theorem RatFunc.num_div {K : Type u} [Field K] (p : Polynomial K) (q : Polynomial K) :
                                                      RatFunc.num ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) = Polynomial.C (Polynomial.leadingCoeff (q / gcd p q))⁻¹ * (p / gcd p q)
                                                      @[simp]
                                                      theorem RatFunc.num_one {K : Type u} [Field K] :
                                                      @[simp]
                                                      theorem RatFunc.num_div_dvd {K : Type u} [Field K] (p : Polynomial K) {q : Polynomial K} (hq : q 0) :
                                                      @[simp]
                                                      theorem RatFunc.num_div_dvd' {K : Type u} [Field K] (p : Polynomial K) {q : Polynomial K} (hq : q 0) :
                                                      Polynomial.C (Polynomial.leadingCoeff (q / gcd p q))⁻¹ * (p / gcd p q) p

                                                      A version of num_div_dvd with the LHS in simp normal form

                                                      def RatFunc.denom {K : Type u} [Field K] (x : RatFunc K) :

                                                      RatFunc.denom is the denominator of a rational function, normalized such that it is monic.

                                                      Equations
                                                      Instances For
                                                        @[simp]
                                                        theorem RatFunc.denom_div {K : Type u} [Field K] (p : Polynomial K) {q : Polynomial K} (hq : q 0) :
                                                        RatFunc.denom ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) = Polynomial.C (Polynomial.leadingCoeff (q / gcd p q))⁻¹ * (q / gcd p q)
                                                        @[simp]
                                                        theorem RatFunc.denom_zero {K : Type u} [Field K] :
                                                        @[simp]
                                                        theorem RatFunc.denom_one {K : Type u} [Field K] :
                                                        @[simp]
                                                        @[simp]
                                                        @[simp]
                                                        theorem RatFunc.num_eq_zero_iff {K : Type u} [Field K] {x : RatFunc K} :
                                                        RatFunc.num x = 0 x = 0
                                                        theorem RatFunc.num_ne_zero {K : Type u} [Field K] {x : RatFunc K} (hx : x 0) :
                                                        theorem RatFunc.num_mul_eq_mul_denom_iff {K : Type u} [Field K] {x : RatFunc K} {p : Polynomial K} {q : Polynomial K} (hq : q 0) :
                                                        theorem RatFunc.num_dvd {K : Type u} [Field K] {x : RatFunc K} {p : Polynomial K} (hp : p 0) :
                                                        RatFunc.num x p ∃ (q : Polynomial K), q 0 x = (algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q
                                                        theorem RatFunc.denom_dvd {K : Type u} [Field K] {x : RatFunc K} {q : Polynomial K} (hq : q 0) :
                                                        theorem RatFunc.map_denom_ne_zero {K : Type u} [Field K] {L : Type u_1} {F : Type u_2} [Zero L] [FunLike F (Polynomial K) L] [ZeroHomClass F (Polynomial K) L] (φ : F) (hφ : Function.Injective φ) (f : RatFunc K) :
                                                        theorem RatFunc.map_apply {K : Type u} [Field K] {R : Type u_1} {F : Type u_2} [CommRing R] [IsDomain R] [FunLike F (Polynomial K) (Polynomial R)] [MonoidHomClass F (Polynomial K) (Polynomial R)] (φ : F) (hφ : nonZeroDivisors (Polynomial K) Submonoid.comap φ (nonZeroDivisors (Polynomial R))) (f : RatFunc K) :
                                                        theorem RatFunc.liftAlgHom_apply {K : Type u} [Field K] {L : Type u_1} {S : Type u_2} [Field L] [CommSemiring S] [Algebra S (Polynomial K)] [Algebra S L] (φ : Polynomial K →ₐ[S] L) (hφ : nonZeroDivisors (Polynomial K) Submonoid.comap φ (nonZeroDivisors L)) (f : RatFunc K) :

                                                        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] :
                                                          RingHom.comp (algebraMap (Polynomial K) (RatFunc K)) 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.num (RatFunc.C c) = Polynomial.C c
                                                            @[simp]
                                                            theorem RatFunc.denom_C {K : Type u} [Field K] (c : K) :
                                                            RatFunc.denom (RatFunc.C c) = 1
                                                            @[simp]
                                                            theorem RatFunc.num_X {K : Type u} [Field K] :
                                                            RatFunc.num RatFunc.X = Polynomial.X
                                                            @[simp]
                                                            theorem RatFunc.denom_X {K : Type u} [Field K] :
                                                            RatFunc.denom RatFunc.X = 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_1} [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_1} [Field L] {f : K →+* L} {a : L} {x : RatFunc K} (h : Polynomial.eval₂ f a (RatFunc.denom x) = 0) :
                                                              RatFunc.eval f a x = 0
                                                              theorem RatFunc.eval₂_denom_ne_zero {K : Type u} [Field K] {L : Type u_1} [Field L] {f : K →+* L} {a : L} {x : RatFunc K} (h : RatFunc.eval f a x 0) :
                                                              @[simp]
                                                              theorem RatFunc.eval_C {K : Type u} [Field K] {L : Type u_1} [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_1} [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_1} [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_1} [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_1} [Field L] (f : K →+* L) (a : L) {S : Type u_2} [CommSemiring S] [Algebra S (Polynomial K)] (p : S) :
                                                              theorem RatFunc.eval_add {K : Type u} [Field K] {L : Type u_1} [Field L] (f : K →+* L) (a : L) {x : RatFunc K} {y : RatFunc K} (hx : Polynomial.eval₂ f a (RatFunc.denom x) 0) (hy : Polynomial.eval₂ f a (RatFunc.denom y) 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_1} [Field L] (f : K →+* L) (a : L) {x : RatFunc K} {y : RatFunc K} (hx : Polynomial.eval₂ f a (RatFunc.denom x) 0) (hy : Polynomial.eval₂ f a (RatFunc.denom y) 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.

                                                              def RatFunc.intDegree {K : Type u} [Field K] (x : RatFunc K) :

                                                              intDegree x is the degree of the rational function x, defined as the difference between the natDegree of its numerator and the natDegree of its denominator. In particular, intDegree 0 = 0.

                                                              Equations
                                                              Instances For
                                                                @[simp]
                                                                @[simp]
                                                                @[simp]
                                                                theorem RatFunc.intDegree_C {K : Type u} [Field K] (k : K) :
                                                                RatFunc.intDegree (RatFunc.C k) = 0
                                                                @[simp]
                                                                theorem RatFunc.intDegree_X {K : Type u} [Field K] :
                                                                RatFunc.intDegree RatFunc.X = 1
                                                                theorem RatFunc.intDegree_mul {K : Type u} [Field K] {x : RatFunc K} {y : RatFunc K} (hx : x 0) (hy : y 0) :
                                                                theorem RatFunc.intDegree_add_le {K : Type u} [Field K] {x : RatFunc K} {y : RatFunc K} (hy : y 0) (hxy : x + y 0) :

                                                                The coercion RatFunc F → LaurentSeries F as bundled alg hom.

                                                                Equations
                                                                Instances For

                                                                  The coercion RatFunc F → LaurentSeries F as a function.

                                                                  This is the implementation of coeToLaurentSeries.

                                                                  Equations
                                                                  Instances For
                                                                    Equations
                                                                    • RatFunc.coeToLaurentSeries = { coe := RatFunc.coeToLaurentSeries_fun }
                                                                    theorem RatFunc.coe_def {F : Type u} [Field F] (f : RatFunc F) :
                                                                    f = (RatFunc.coeAlgHom F) f
                                                                    theorem RatFunc.coe_injective {F : Type u} [Field F] :
                                                                    Function.Injective RatFunc.coeToLaurentSeries_fun
                                                                    @[simp]
                                                                    theorem RatFunc.coe_apply {F : Type u} [Field F] (f : RatFunc F) :
                                                                    (RatFunc.coeAlgHom F) f = f
                                                                    @[simp]
                                                                    theorem RatFunc.coe_zero {F : Type u} [Field F] :
                                                                    0 = 0
                                                                    @[simp]
                                                                    theorem RatFunc.coe_one {F : Type u} [Field F] :
                                                                    1 = 1
                                                                    @[simp]
                                                                    theorem RatFunc.coe_add {F : Type u} [Field F] (f : RatFunc F) (g : RatFunc F) :
                                                                    (f + g) = f + g
                                                                    @[simp]
                                                                    theorem RatFunc.coe_sub {F : Type u} [Field F] (f : RatFunc F) (g : RatFunc F) :
                                                                    (f - g) = f - g
                                                                    @[simp]
                                                                    theorem RatFunc.coe_neg {F : Type u} [Field F] (f : RatFunc F) :
                                                                    (-f) = -f
                                                                    @[simp]
                                                                    theorem RatFunc.coe_mul {F : Type u} [Field F] (f : RatFunc F) (g : RatFunc F) :
                                                                    (f * g) = f * g
                                                                    @[simp]
                                                                    theorem RatFunc.coe_pow {F : Type u} [Field F] (f : RatFunc F) (n : ) :
                                                                    (f ^ n) = f ^ n
                                                                    @[simp]
                                                                    theorem RatFunc.coe_div {F : Type u} [Field F] (f : RatFunc F) (g : RatFunc F) :
                                                                    (f / g) = f / g
                                                                    @[simp]
                                                                    theorem RatFunc.coe_C {F : Type u} [Field F] (r : F) :
                                                                    (RatFunc.C r) = HahnSeries.C r
                                                                    @[simp]
                                                                    theorem RatFunc.coe_smul {F : Type u} [Field F] (f : RatFunc F) (r : F) :
                                                                    (r f) = r f
                                                                    @[simp]
                                                                    theorem RatFunc.coe_X {F : Type u} [Field F] :
                                                                    RatFunc.X = (HahnSeries.single 1) 1