Documentation

Mathlib.FieldTheory.RatFunc.Basic

The field structure of rational functions #

Main definitions #

Working with rational functions as polynomials:

Working with rational functions as fractions:

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 lifting homomorphisms of polynomials to other polynomials, with the same condition on retaining the non-zero-divisor property across the map:

theorem RatFunc.zero_def {K : Type u_1} [CommRing K] :
RatFunc.zero = { toFractionRing := 0 }
@[irreducible]
def RatFunc.zero {K : Type u_1} [CommRing K] :

The zero rational function.

Equations
Instances For
    instance RatFunc.instZero {K : Type u} [CommRing K] :
    Equations
    • RatFunc.instZero = { zero := RatFunc.zero }
    theorem RatFunc.ofFractionRing_zero {K : Type u} [CommRing K] :
    { toFractionRing := 0 } = 0
    @[irreducible]
    def RatFunc.add {K : Type u_1} [CommRing K] :
    RatFunc KRatFunc KRatFunc K

    Addition of rational functions.

    Equations
    Instances For
      theorem RatFunc.add_def {K : Type u_1} [CommRing K] :
      ∀ (x x_1 : RatFunc K), x.add x_1 = match x, x_1 with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p + q }
      instance RatFunc.instAdd {K : Type u} [CommRing K] :
      Equations
      • RatFunc.instAdd = { 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), x.sub 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.instSub {K : Type u} [CommRing K] :
        Equations
        • RatFunc.instSub = { 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), x.neg = 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.instNeg {K : Type u} [CommRing K] :
          Equations
          • RatFunc.instNeg = { 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.instOne {K : Type u} [CommRing K] :
            Equations
            • RatFunc.instOne = { one := RatFunc.one }
            theorem RatFunc.ofFractionRing_one {K : Type u} [CommRing K] :
            { toFractionRing := 1 } = 1
            theorem RatFunc.mul_def {K : Type u_1} [CommRing K] :
            ∀ (x x_1 : RatFunc K), x.mul x_1 = match x, x_1 with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p * q }
            @[irreducible]
            def RatFunc.mul {K : Type u_1} [CommRing K] :
            RatFunc KRatFunc KRatFunc K

            Multiplication of rational functions.

            Equations
            Instances For
              instance RatFunc.instMul {K : Type u} [CommRing K] :
              Equations
              • RatFunc.instMul = { 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 }
              @[irreducible]
              def RatFunc.div {K : Type u_1} [CommRing K] [IsDomain K] :
              RatFunc KRatFunc KRatFunc K

              Division of rational functions.

              Equations
              Instances For
                theorem RatFunc.div_def {K : Type u_1} [CommRing K] [IsDomain K] :
                ∀ (x x_1 : RatFunc K), x.div x_1 = match x, x_1 with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p / q }
                instance RatFunc.instDiv {K : Type u} [CommRing K] [IsDomain K] :
                Equations
                • RatFunc.instDiv = { 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), x.inv = match x with | { toFractionRing := p } => { toFractionRing := p⁻¹ }
                  instance RatFunc.instInv {K : Type u} [CommRing K] [IsDomain K] :
                  Equations
                  • RatFunc.instInv = { 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
                  @[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
                    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 }
                    Equations
                    • RatFunc.instSMulOfFractionRingPolynomial = { 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
                    • =
                    Equations
                    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 = { 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) φ d, }

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

                                      The coercion from polynomials to rational functions, implemented as the algebra map from a domain to its field of fractions

                                      Equations
                                      Instances For
                                        Equations
                                        • RatFunc.instCoePolynomial = { coe := RatFunc.coePolynomial }
                                        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

                                            RatFunc K is the field of fractions of the polynomials over K.

                                            Equations
                                            • =
                                            @[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') ) :
                                            ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q).liftOn f H = 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) :
                                            ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q).liftOn' f H = 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.

                                            theorem RatFunc.mk_eq_mk' {K : Type u} [CommRing K] [IsDomain K] (f : Polynomial K) {g : Polynomial K} (hg : g 0) :
                                            RatFunc.mk f g = IsLocalization.mk' (RatFunc K) f g,
                                            @[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) :
                                              ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q).numDenom = (Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q), Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (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
                                              • x.num = x.numDenom.1
                                              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) :
                                                ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q).num = Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)
                                                @[simp]
                                                theorem RatFunc.num_one {K : Type u} [Field K] :
                                                @[simp]
                                                theorem RatFunc.num_algebraMap {K : Type u} [Field K] (p : Polynomial K) :
                                                ((algebraMap (Polynomial K) (RatFunc K)) p).num = p
                                                theorem RatFunc.num_div_dvd {K : Type u} [Field K] (p : Polynomial K) {q : Polynomial K} (hq : q 0) :
                                                ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q).num p
                                                @[simp]
                                                theorem RatFunc.num_div_dvd' {K : Type u} [Field K] (p : Polynomial K) {q : Polynomial K} (hq : q 0) :
                                                Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (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
                                                • x.denom = x.numDenom.2
                                                Instances For
                                                  @[simp]
                                                  theorem RatFunc.denom_div {K : Type u} [Field K] (p : Polynomial K) {q : Polynomial K} (hq : q 0) :
                                                  ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q).denom = Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q)
                                                  theorem RatFunc.monic_denom {K : Type u} [Field K] (x : RatFunc K) :
                                                  x.denom.Monic
                                                  theorem RatFunc.denom_ne_zero {K : Type u} [Field K] (x : RatFunc K) :
                                                  x.denom 0
                                                  @[simp]
                                                  theorem RatFunc.denom_zero {K : Type u} [Field K] :
                                                  @[simp]
                                                  theorem RatFunc.denom_one {K : Type u} [Field K] :
                                                  @[simp]
                                                  theorem RatFunc.denom_algebraMap {K : Type u} [Field K] (p : Polynomial K) :
                                                  ((algebraMap (Polynomial K) (RatFunc K)) p).denom = 1
                                                  @[simp]
                                                  theorem RatFunc.denom_div_dvd {K : Type u} [Field K] (p : Polynomial K) (q : Polynomial K) :
                                                  ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q).denom q
                                                  @[simp]
                                                  theorem RatFunc.num_div_denom {K : Type u} [Field K] (x : RatFunc K) :
                                                  (algebraMap (Polynomial K) (RatFunc K)) x.num / (algebraMap (Polynomial K) (RatFunc K)) x.denom = x
                                                  theorem RatFunc.isCoprime_num_denom {K : Type u} [Field K] (x : RatFunc K) :
                                                  IsCoprime x.num x.denom
                                                  @[simp]
                                                  theorem RatFunc.num_eq_zero_iff {K : Type u} [Field K] {x : RatFunc K} :
                                                  x.num = 0 x = 0
                                                  theorem RatFunc.num_ne_zero {K : Type u} [Field K] {x : RatFunc K} (hx : x 0) :
                                                  x.num 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) :
                                                  x.num * q = p * x.denom x = (algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q
                                                  theorem RatFunc.num_denom_add {K : Type u} [Field K] (x : RatFunc K) (y : RatFunc K) :
                                                  (x + y).num * (x.denom * y.denom) = (x.num * y.denom + x.denom * y.num) * (x + y).denom
                                                  theorem RatFunc.num_denom_neg {K : Type u} [Field K] (x : RatFunc K) :
                                                  (-x).num * x.denom = -x.num * (-x).denom
                                                  theorem RatFunc.num_denom_mul {K : Type u} [Field K] (x : RatFunc K) (y : RatFunc K) :
                                                  (x * y).num * (x.denom * y.denom) = x.num * y.num * (x * y).denom
                                                  theorem RatFunc.num_dvd {K : Type u} [Field K] {x : RatFunc K} {p : Polynomial K} (hp : p 0) :
                                                  x.num 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) :
                                                  x.denom q ∃ (p : Polynomial K), x = (algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q
                                                  theorem RatFunc.num_mul_dvd {K : Type u} [Field K] (x : RatFunc K) (y : RatFunc K) :
                                                  (x * y).num x.num * y.num
                                                  theorem RatFunc.denom_mul_dvd {K : Type u} [Field K] (x : RatFunc K) (y : RatFunc K) :
                                                  (x * y).denom x.denom * y.denom
                                                  theorem RatFunc.denom_add_dvd {K : Type u} [Field K] (x : RatFunc K) (y : RatFunc K) :
                                                  (x + y).denom x.denom * y.denom
                                                  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) :
                                                  φ f.denom 0
                                                  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) :
                                                  (RatFunc.map φ ) f = (algebraMap (Polynomial R) (RatFunc R)) (φ f.num) / (algebraMap (Polynomial R) (RatFunc R)) (φ f.denom)
                                                  theorem RatFunc.liftRingHom_apply {K : Type u} [Field K] {L : Type u_1} [Field L] (φ : Polynomial K →+* L) (hφ : nonZeroDivisors (Polynomial K) Submonoid.comap φ (nonZeroDivisors L)) (f : RatFunc K) :
                                                  (RatFunc.liftRingHom φ ) f = φ f.num / φ f.denom
                                                  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) :
                                                  (RatFunc.liftAlgHom φ ) f = φ f.num / φ f.denom
                                                  theorem RatFunc.num_mul_denom_add_denom_mul_num_ne_zero {K : Type u} [Field K] {x : RatFunc K} {y : RatFunc K} (hxy : x + y 0) :
                                                  x.num * y.denom + x.denom * y.num 0