# The field structure of rational functions #

## Main definitions #

Working with rational functions as polynomials:

• RatFunc.instField provides a field structure You can use IsFractionRing API to treat RatFunc as the field of fractions of polynomials:
• algebraMap K[X] (RatFunc K) maps polynomials to rational functions
• IsFractionRing.algEquiv maps other fields of fractions of K[X] to RatFunc K, in particular:
• FractionRing.algEquiv K[X] (RatFunc K) maps the generic field of fraction construction to RatFunc K. Combine this with AlgEquiv.restrictScalars to change the FractionRing K[X] ≃ₐ[K[X]] RatFunc K to FractionRing K[X] ≃ₐ[K] RatFunc K.

Working with rational functions as fractions:

• RatFunc.num and RatFunc.denom give the numerator and denominator. These values are chosen to be coprime and such that RatFunc.denom is monic.

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

• RatFunc.liftMonoidWithZeroHom lifts a K[X] →*₀ G₀ to a RatFunc K →*₀ G₀, where [CommRing K] [CommGroupWithZero G₀]
• RatFunc.liftRingHom lifts a K[X] →+* L to a RatFunc K →+* L, where [CommRing K] [Field L]
• RatFunc.liftAlgHom lifts a K[X] →ₐ[S] L to a RatFunc K →ₐ[S] L, where [CommRing K] [Field L] [CommSemiring S] [Algebra S K[X]] [Algebra S L] This is satisfied by injective homs.

We also have lifting homomorphisms of polynomials to other polynomials, with the same condition on retaining the non-zero-divisor property across the map:

• RatFunc.map lifts K[X] →* R[X] when [CommRing K] [CommRing R]
• RatFunc.mapRingHom lifts K[X] →+* R[X] when [CommRing K] [CommRing R]
• RatFunc.mapAlgHom lifts K[X] →ₐ[S] R[X] when [CommRing K] [IsDomain K] [CommRing R] [IsDomain R]
theorem RatFunc.zero_def {K : Type u_1} [] :
RatFunc.zero = { toFractionRing := 0 }
@[irreducible]
def RatFunc.zero {K : Type u_1} [] :

The zero rational function.

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

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

Subtraction of rational functions.

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

Additive inverse of a rational function.

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

The multiplicative unit of rational functions.

Equations
Instances For
instance RatFunc.instOne {K : Type u} [] :
Equations
• RatFunc.instOne = { one := RatFunc.one }
theorem RatFunc.ofFractionRing_one {K : Type u} [] :
{ toFractionRing := 1 } = 1
theorem RatFunc.mul_def {K : Type u_1} [] :
∀ (x x_1 : ), x.mul x_1 = match x, x_1 with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p * q }
@[irreducible]
def RatFunc.mul {K : Type u_1} [] :

Multiplication of rational functions.

Equations
Instances For
instance RatFunc.instMul {K : Type u} [] :
Equations
• RatFunc.instMul = { mul := RatFunc.mul }
theorem RatFunc.ofFractionRing_mul {K : Type u} [] (p : ) (q : ) :
{ toFractionRing := p * q } = { toFractionRing := p } * { toFractionRing := q }
@[irreducible]
def RatFunc.div {K : Type u_1} [] [] :

Division of rational functions.

Equations
Instances For
theorem RatFunc.div_def {K : Type u_1} [] [] :
∀ (x x_1 : ), x.div x_1 = match x, x_1 with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p / q }
instance RatFunc.instDiv {K : Type u} [] [] :
Equations
• RatFunc.instDiv = { div := RatFunc.div }
theorem RatFunc.ofFractionRing_div {K : Type u} [] [] (p : ) (q : ) :
{ toFractionRing := p / q } = { toFractionRing := p } / { toFractionRing := q }
@[irreducible]
def RatFunc.inv {K : Type u_1} [] [] :

Multiplicative inverse of a rational function.

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

Scalar multiplication of rational functions.

Equations
Instances For
theorem RatFunc.smul_def {K : Type u_2} [] {R : Type u_3} [SMul R (FractionRing (Polynomial K))] :
∀ (x : R) (x_1 : ), 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} [] {R : Type u_1} [SMul R (FractionRing (Polynomial K))] (c : R) (p : ) :
{ toFractionRing := c p } = c { toFractionRing := p }
theorem RatFunc.toFractionRing_smul {K : Type u} [] {R : Type u_1} [SMul R (FractionRing (Polynomial K))] (c : R) (p : ) :
(c p).toFractionRing = c p.toFractionRing
theorem RatFunc.smul_eq_C_smul {K : Type u} [] (x : ) (r : K) :
r x = Polynomial.C r x
theorem RatFunc.mk_smul {K : Type u} [] {R : Type u_1} [] [] [] [IsScalarTower R (Polynomial K) (Polynomial K)] (c : R) (p : ) (q : ) :
RatFunc.mk (c p) q = c
Equations
• =
instance RatFunc.instSubsingleton (K : Type u) [] [] :
Equations
• =
instance RatFunc.instInhabited (K : Type u) [] :
Equations
• = { default := 0 }
instance RatFunc.instNontrivial (K : Type u) [] [] :
Equations
• =
@[simp]
theorem RatFunc.toFractionRingRingEquiv_apply (K : Type u) [] (self : ) :
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
• = { 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
def RatFunc.instCommMonoid (K : Type u) [] :

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
instance RatFunc.instCommRing (K : Type u) [] :
Equations
• = let __src := ; let __src_1 := ;
def RatFunc.map {R : Type u_3} {S : Type u_4} {F : Type u_5} [] [] [FunLike F (Polynomial R) (Polynomial S)] [MonoidHomClass F (Polynomial R) (Polynomial S)] (φ : F) (hφ : ) :

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} [] [] [FunLike F (Polynomial R) (Polynomial S)] [MonoidHomClass F (Polynomial R) (Polynomial S)] (φ : F) (hφ : ) (n : ) (d : ) :
(RatFunc.map φ ) { toFractionRing := } = { toFractionRing := Localization.mk (φ n) φ d, }
theorem RatFunc.map_injective {R : Type u_3} {S : Type u_4} {F : Type u_5} [] [] [FunLike F (Polynomial R) (Polynomial S)] [MonoidHomClass F (Polynomial R) (Polynomial S)] (φ : F) (hφ : ) (hf : ) :
def RatFunc.mapRingHom {R : Type u_3} {S : Type u_4} {F : Type u_5} [] [] [FunLike F (Polynomial R) (Polynomial S)] [RingHomClass F (Polynomial R) (Polynomial S)] (φ : F) (hφ : ) :

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
• = let __src := RatFunc.map φ ; { toMonoidHom := __src, map_zero' := , map_add' := }
Instances For
theorem RatFunc.coe_mapRingHom_eq_coe_map {R : Type u_3} {S : Type u_4} {F : Type u_5} [] [] [FunLike F (Polynomial R) (Polynomial S)] [RingHomClass F (Polynomial R) (Polynomial S)] (φ : F) (hφ : ) :
(RatFunc.mapRingHom φ ) = (RatFunc.map φ )
def RatFunc.liftMonoidWithZeroHom {G₀ : Type u_1} {R : Type u_3} [] [] (φ : →*₀ G₀) (hφ : ) :
→*₀ G₀

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
• = { toFun := fun (f : ) => f.liftOn (fun (p q : ) => φ p / φ q) , map_zero' := , map_one' := , map_mul' := }
Instances For
theorem RatFunc.liftMonoidWithZeroHom_apply_ofFractionRing_mk {G₀ : Type u_1} {R : Type u_3} [] [] (φ : →*₀ G₀) (hφ : ) (n : ) (d : ) :
{ toFractionRing := } = φ n / φ d
theorem RatFunc.liftMonoidWithZeroHom_injective {G₀ : Type u_1} {R : Type u_3} [] [] [] (φ : →*₀ G₀) (hφ : ) (hφ' : optParam ( ) ) :
def RatFunc.liftRingHom {L : Type u_2} {R : Type u_3} [] [] (φ : ) (hφ : ) :

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

Equations
• = let __src := RatFunc.liftMonoidWithZeroHom φ.toMonoidWithZeroHom ; { toFun := (↑__src).toFun, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
theorem RatFunc.liftRingHom_apply_ofFractionRing_mk {L : Type u_2} {R : Type u_3} [] [] (φ : ) (hφ : ) (n : ) (d : ) :
(RatFunc.liftRingHom φ ) { toFractionRing := } = φ n / φ d
theorem RatFunc.liftRingHom_injective {L : Type u_2} {R : Type u_3} [] [] [] (φ : ) (hφ : ) (hφ' : optParam ( ) ) :
instance RatFunc.instField (K : Type u) [] [] :
Equations
• = Field.mk zpowRec (fun (q : ℚ≥0) => ) (fun (a : ) => )

### RatFunc as field of fractions of Polynomial#

instance RatFunc.instAlgebraOfPolynomial (K : Type u) [] [] (R : Type u_1) [] [Algebra R (Polynomial K)] :
Equations
• One or more equations did not get rendered due to their size.
def RatFunc.coePolynomial {K : Type u} [] [] (P : ) :

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

Equations
Instances For
instance RatFunc.instCoePolynomial {K : Type u} [] [] :
Equations
• RatFunc.instCoePolynomial = { coe := RatFunc.coePolynomial }
theorem RatFunc.mk_one {K : Type u} [] [] (x : ) :
theorem RatFunc.ofFractionRing_algebraMap {K : Type u} [] [] (x : ) :
{ toFractionRing := (algebraMap (Polynomial K) (FractionRing (Polynomial K))) x } = (algebraMap (Polynomial K) (RatFunc K)) x
@[simp]
theorem RatFunc.mk_eq_div {K : Type u} [] [] (p : ) (q : ) :
@[simp]
theorem RatFunc.div_smul {K : Type u} [] [] {R : Type u_1} [] [] [IsScalarTower R (Polynomial K) (Polynomial K)] (c : R) (p : ) (q : ) :
theorem RatFunc.algebraMap_apply {K : Type u} [] [] {R : Type u_1} [] [Algebra R (Polynomial K)] (x : R) :
theorem RatFunc.map_apply_div_ne_zero {K : Type u} [] [] {R : Type u_1} {F : Type u_2} [] [] [FunLike F (Polynomial K) (Polynomial R)] [MonoidHomClass F (Polynomial K) (Polynomial R)] (φ : F) (hφ : ) (p : ) (q : ) (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]
theorem RatFunc.map_apply_div {K : Type u} [] [] {R : Type u_1} {F : Type u_2} [] [] [FunLike F (Polynomial K) (Polynomial R)] [] (φ : F) (hφ : ) (p : ) (q : ) :
(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)
theorem RatFunc.liftMonoidWithZeroHom_apply_div {K : Type u} [] [] {L : Type u_1} (φ : ) (hφ : ) (p : ) (q : ) :
((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) = φ p / φ q
@[simp]
theorem RatFunc.liftMonoidWithZeroHom_apply_div' {K : Type u} [] [] {L : Type u_1} (φ : ) (hφ : ) (p : ) (q : ) :
((algebraMap (Polynomial K) (RatFunc K)) p) / ((algebraMap (Polynomial K) (RatFunc K)) q) = φ p / φ q
theorem RatFunc.liftRingHom_apply_div {K : Type u} [] [] {L : Type u_1} [] (φ : ) (hφ : ) (p : ) (q : ) :
(RatFunc.liftRingHom φ ) ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) = φ p / φ q
@[simp]
theorem RatFunc.liftRingHom_apply_div' {K : Type u} [] [] {L : Type u_1} [] (φ : ) (hφ : ) (p : ) (q : ) :
(RatFunc.liftRingHom φ ) ((algebraMap (Polynomial K) (RatFunc K)) p) / (RatFunc.liftRingHom φ ) ((algebraMap (Polynomial K) (RatFunc K)) q) = φ p / φ q
theorem RatFunc.ofFractionRing_comp_algebraMap (K : Type u) [] [] :
RatFunc.ofFractionRing (algebraMap (Polynomial K) (FractionRing (Polynomial K))) = (algebraMap (Polynomial K) (RatFunc K))
@[simp]
theorem RatFunc.algebraMap_eq_zero_iff (K : Type u) [] [] {x : } :
(algebraMap (Polynomial K) (RatFunc K)) x = 0 x = 0
theorem RatFunc.algebraMap_ne_zero {K : Type u} [] [] {x : } (hx : x 0) :
def RatFunc.mapAlgHom {K : Type u} [] [] {R : Type u_2} {S : Type u_3} [] [] [] [Algebra S (Polynomial K)] [Algebra S (Polynomial R)] (φ : ) (hφ : ) :

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
• = let __src := ; { toRingHom := __src, commutes' := }
Instances For
theorem RatFunc.coe_mapAlgHom_eq_coe_map {K : Type u} [] [] {R : Type u_2} {S : Type u_3} [] [] [] [Algebra S (Polynomial K)] [Algebra S (Polynomial R)] (φ : ) (hφ : ) :
(RatFunc.mapAlgHom φ ) = (RatFunc.map φ )
def RatFunc.liftAlgHom {K : Type u} [] [] {L : Type u_1} {S : Type u_3} [] [] [Algebra S (Polynomial K)] [Algebra S L] (φ : →ₐ[S] L) (hφ : ) :

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} [] [] {L : Type u_1} {S : Type u_3} [] [] [Algebra S (Polynomial K)] [Algebra S L] (φ : →ₐ[S] L) (hφ : ) (n : ) (d : ) :
(RatFunc.liftAlgHom φ ) { toFractionRing := } = φ n / φ d
theorem RatFunc.liftAlgHom_injective {K : Type u} [] [] {L : Type u_1} {S : Type u_3} [] [] [Algebra S (Polynomial K)] [Algebra S L] (φ : →ₐ[S] L) (hφ : ) (hφ' : optParam ( ) ) :
@[simp]
theorem RatFunc.liftAlgHom_apply_div' {K : Type u} [] [] {L : Type u_1} {S : Type u_3} [] [] [Algebra S (Polynomial K)] [Algebra S L] (φ : →ₐ[S] L) (hφ : ) (p : ) (q : ) :
(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} [] [] {L : Type u_1} {S : Type u_3} [] [] [Algebra S (Polynomial K)] [Algebra S L] (φ : →ₐ[S] L) (hφ : ) (p : ) (q : ) :
(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} [] [] {P : Sort v} (p : ) (q : ) (f : P) (f0 : ∀ (p : ), f p 0 = f 0 1) (H' : ∀ {p q p' q' : }, q 0q' 0q' * p = q * p'f p q = f p' q') (H : optParam (∀ {p q p' q' : }, q' 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} [] [] {P : Sort v} (p : ) (q : ) (f : P) (f0 : ∀ (p : ), f p 0 = f 0 1) (H : ∀ {p q a : }, 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} [] [] {P : Prop} (x : ) (f : ∀ (p q : ), 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.ofFractionRing_mk' {K : Type u} [] [] (x : ) (y : ) :
{ toFractionRing := } =
theorem RatFunc.mk_eq_mk' {K : Type u} [] [] (f : ) {g : } (hg : g 0) :
= IsLocalization.mk' (RatFunc K) f g,
@[simp]
theorem RatFunc.ofFractionRing_eq {K : Type u} [] [] :
RatFunc.ofFractionRing = (IsLocalization.algEquiv (FractionRing (Polynomial K)) (RatFunc K))
@[simp]
theorem RatFunc.toFractionRing_eq {K : Type u} [] [] :
RatFunc.toFractionRing = (IsLocalization.algEquiv (RatFunc K) (FractionRing (Polynomial K)))

### Numerator and denominator #

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

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} [] (p : ) {q : } (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} [] (x : ) :

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} [] :
= 0
@[simp]
theorem RatFunc.num_div {K : Type u} [] (p : ) (q : ) :
((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} [] :
= 1
@[simp]
theorem RatFunc.num_algebraMap {K : Type u} [] (p : ) :
((algebraMap (Polynomial K) (RatFunc K)) p).num = p
theorem RatFunc.num_div_dvd {K : Type u} [] (p : ) {q : } (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} [] (p : ) {q : } (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} [] (x : ) :

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} [] (p : ) {q : } (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} [] (x : ) :
x.denom.Monic
theorem RatFunc.denom_ne_zero {K : Type u} [] (x : ) :
x.denom 0
@[simp]
theorem RatFunc.denom_zero {K : Type u} [] :
@[simp]
theorem RatFunc.denom_one {K : Type u} [] :
@[simp]
theorem RatFunc.denom_algebraMap {K : Type u} [] (p : ) :
((algebraMap (Polynomial K) (RatFunc K)) p).denom = 1
@[simp]
theorem RatFunc.denom_div_dvd {K : Type u} [] (p : ) (q : ) :
((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q).denom q
@[simp]
theorem RatFunc.num_div_denom {K : Type u} [] (x : ) :
(algebraMap (Polynomial K) (RatFunc K)) x.num / (algebraMap (Polynomial K) (RatFunc K)) x.denom = x
theorem RatFunc.isCoprime_num_denom {K : Type u} [] (x : ) :
IsCoprime x.num x.denom
@[simp]
theorem RatFunc.num_eq_zero_iff {K : Type u} [] {x : } :
x.num = 0 x = 0
theorem RatFunc.num_ne_zero {K : Type u} [] {x : } (hx : x 0) :
x.num 0
theorem RatFunc.num_mul_eq_mul_denom_iff {K : Type u} [] {x : } {p : } {q : } (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} [] (x : ) (y : ) :
(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} [] (x : ) :
(-x).num * x.denom = -x.num * (-x).denom
theorem RatFunc.num_denom_mul {K : Type u} [] (x : ) (y : ) :
(x * y).num * (x.denom * y.denom) = x.num * y.num * (x * y).denom
theorem RatFunc.num_dvd {K : Type u} [] {x : } {p : } (hp : p 0) :
x.num p ∃ (q : ), q 0 x = (algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q
theorem RatFunc.denom_dvd {K : Type u} [] {x : } {q : } (hq : q 0) :
x.denom q ∃ (p : ), x = (algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q
theorem RatFunc.num_mul_dvd {K : Type u} [] (x : ) (y : ) :
(x * y).num x.num * y.num
theorem RatFunc.denom_mul_dvd {K : Type u} [] (x : ) (y : ) :
(x * y).denom x.denom * y.denom
theorem RatFunc.denom_add_dvd {K : Type u} [] (x : ) (y : ) :
(x + y).denom x.denom * y.denom
theorem RatFunc.map_denom_ne_zero {K : Type u} [] {L : Type u_1} {F : Type u_2} [Zero L] [FunLike F (Polynomial K) L] [ZeroHomClass F (Polynomial K) L] (φ : F) (hφ : ) (f : ) :
φ f.denom 0
theorem RatFunc.map_apply {K : Type u} [] {R : Type u_1} {F : Type u_2} [] [] [FunLike F (Polynomial K) (Polynomial R)] [MonoidHomClass F (Polynomial K) (Polynomial R)] (φ : F) (hφ : ) (f : ) :
(RatFunc.map φ ) f = (algebraMap (Polynomial R) (RatFunc R)) (φ f.num) / (algebraMap (Polynomial R) (RatFunc R)) (φ f.denom)
theorem RatFunc.liftMonoidWithZeroHom_apply {K : Type u} [] {L : Type u_1} (φ : ) (hφ : ) (f : ) :
f = φ f.num / φ f.denom
theorem RatFunc.liftRingHom_apply {K : Type u} [] {L : Type u_1} [] (φ : ) (hφ : ) (f : ) :
(RatFunc.liftRingHom φ ) f = φ f.num / φ f.denom
theorem RatFunc.liftAlgHom_apply {K : Type u} [] {L : Type u_1} {S : Type u_2} [] [] [Algebra S (Polynomial K)] [Algebra S L] (φ : →ₐ[S] L) (hφ : ) (f : ) :
(RatFunc.liftAlgHom φ ) f = φ f.num / φ f.denom
theorem RatFunc.num_mul_denom_add_denom_mul_num_ne_zero {K : Type u} [] {x : } {y : } (hxy : x + y 0) :
x.num * y.denom + x.denom * y.num 0