# mathlibdocumentation

field_theory.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 `polynomial K`.

## Main definitions #

Working with rational functions as polynomials:

• `ratfunc.field` provides a field structure
• `ratfunc.C` is the constant polynomial
• `ratfunc.X` is the indeterminate
• `ratfunc.eval` evaluates a rational function given a value for the indeterminate You can use `is_fraction_ring` API to treat `ratfunc` as the field of fractions of polynomials:
• `algebra_map K[X] (ratfunc K)` maps polynomials to rational functions
• `is_fraction_ring.alg_equiv` maps other fields of fractions of `polynomial K` to `ratfunc K`, in particular:
• `fraction_ring.alg_equiv K[X] (ratfunc K)` maps the generic field of fraction construction to `ratfunc K`. Combine this with `alg_equiv.restrict_scalars` to change the `fraction_ring K[X] ≃ₐ[polynomial K] ratfunc K` to `fraction_ring 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.

Embedding of rational functions into Laurent series, provided as a coercion, utilizing the underlying `ratfunc.coe_alg_hom`.

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

• `ratfunc.lift_monoid_with_zero_hom` lifts a `polynomial K →*₀ G₀` to a `ratfunc K →*₀ G₀`, where `[comm_ring K] [comm_group_with_zero G₀]`
• `ratfunc.lift_ring_hom` lifts a `polynomial K →+* L` to a `ratfunc K →+* L`, where `[comm_ring K] [field L]`
• `ratfunc.lift_alg_hom` lifts a `polynomial K →ₐ[S] L` to a `ratfunc K →ₐ[S] L`, where `[comm_ring K] [field L] [comm_semiring 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 `polynomial K →* R[X]` when `[comm_ring K] [comm_ring R]`
• `ratfunc.map_ring_hom` lifts `polynomial K →+* R[X]` when `[comm_ring K] [comm_ring R]`
• `ratfunc.map_alg_hom` lifts `polynomial K →ₐ[S] R[X]` when `[comm_ring K] [is_domain K] [comm_ring R] [is_domain R]`

We also have a set of recursion and induction principles:

• `ratfunc.lift_on`: define a function by mapping a fraction of polynomials `p/q` to `f p q`, if `f` is well-defined in the sense that `p/q = p'/q' → f p q = f p' q'`.
• `ratfunc.lift_on'`: define a function by mapping a fraction of polynomials `p/q` to `f p q`, if `f` is well-defined in the sense that `f (a * p) (a * q) = f p' q'`.
• `ratfunc.induction_on`: if `P` holds on `p / q` for all polynomials `p q`, then `P` holds on all rational functions

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

• `int_degree` is the degree of a rational function, defined as the difference between the `nat_degree` of its numerator and the `nat_degree` of its denominator. In particular, `int_degree 0 = 0`.

## Implementation notes #

To provide good API encapsulation and speed up unification problems, `ratfunc` is defined as a structure, and all operations are `@[irreducible] def`s

We need a couple of maps to set up the `field` and `is_fraction_ring` structure, namely `ratfunc.of_fraction_ring`, `ratfunc.to_fraction_ring`, `ratfunc.mk` and `ratfunc.to_fraction_ring_ring_equiv`. All these maps get `simp`ed to bundled morphisms like `algebra_map K[X] (ratfunc K)` and `is_localization.alg_equiv`.

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) [hring : comm_ring K] :
Type u
• to_fraction_ring :

`ratfunc K` is `K(x)`, the field of rational functions over `K`.

The inclusion of polynomials into `ratfunc` is `algebra_map K[X] (ratfunc K)`, the maps between `ratfunc K` and another field of fractions of `polynomial K`, especially `fraction_ring K[X]`, are given by `is_localization.algebra_equiv`.

Instances for `ratfunc`

### Constructing `ratfunc`s and their induction principles #

theorem ratfunc.of_fraction_ring_injective {K : Type u} [hring : comm_ring K] :
function.injective ratfunc.of_fraction_ring
theorem ratfunc.to_fraction_ring_injective {K : Type u} [hring : comm_ring K] :
@[protected]
noncomputable def ratfunc.lift_on {K : Type u} [hring : comm_ring K] {P : Sort v} (x : ratfunc K) (f : → P) (H : ∀ {p q p' q' : , q' p * q' = p' * qf 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 `p * q' = p' * q` 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 `lift_on (p / q) f _ = f p q`.

When `[is_domain K]`, one can use `ratfunc.lift_on'`, 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
theorem ratfunc.lift_on_of_fraction_ring_mk {K : Type u} [hring : comm_ring K] {P : Sort v} (n : polynomial K) (d : ) (f : → P) (H : ∀ {p q p' q' : , q' p * q' = p' * qf p q = f p' q') :
{to_fraction_ring := d}.lift_on f H = f n d
@[protected]
noncomputable def ratfunc.mk {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p 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 `algebra_map _ _ p / algebra_map _ _ q`.

Equations
theorem ratfunc.mk_eq_div' {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p q : polynomial K) :
theorem ratfunc.mk_zero {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : polynomial K) :
theorem ratfunc.mk_coe_def {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : polynomial K) (q : ) :
theorem ratfunc.mk_def_of_mem {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : polynomial K) {q : polynomial K} (hq : q ) :
q = {to_fraction_ring := q, hq⟩}
theorem ratfunc.mk_def_of_ne {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : polynomial K) {q : polynomial K} (hq : q 0) :
q = {to_fraction_ring := q, _⟩}
theorem ratfunc.mk_eq_localization_mk {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : polynomial K) {q : polynomial K} (hq : q 0) :
q = {to_fraction_ring := q, _⟩}
theorem ratfunc.mk_one' {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : polynomial K) :
theorem ratfunc.mk_eq_mk {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {p q p' q' : polynomial K} (hq : q 0) (hq' : q' 0) :
q = q' p * q' = p' * q
theorem ratfunc.lift_on_mk {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {P : Sort v} (p q : polynomial K) (f : → P) (f0 : ∀ (p : , f p 0 = f 0 1) (H' : ∀ {p q p' q' : , q 0q' 0p * q' = p' * qf p q = f p' q') (H : (∀ {p q p' q' : , q' p * q' = p' * qf p q = f p' q') := _) :
q).lift_on f H = f p q
theorem ratfunc.lift_on_condition_of_lift_on'_condition {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {P : Sort v} {f : → P} (H : ∀ {p q a : , q 0a 0f (a * p) (a * q) = f p q) ⦃p q p' q' : polynomial K⦄ (hq : q 0) (hq' : q' 0) (h : p * q' = p' * q) :
f p q = f p' q'
@[protected]
noncomputable def ratfunc.lift_on' {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {P : Sort v} (x : ratfunc K) (f : → P) (H : ∀ {p q a : , 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
theorem ratfunc.lift_on'_mk {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {P : Sort v} (p q : polynomial K) (f : → P) (f0 : ∀ (p : , f p 0 = f 0 1) (H : ∀ {p q a : , q 0a 0f (a * p) (a * q) = f p q) :
q).lift_on' f H = f p q
@[protected]
theorem ratfunc.induction_on' {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {P : → Prop} (x : ratfunc K) (f : ∀ (p q : , q 0P 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 `algebra_map`.

### Defining the field structure #

@[protected]
noncomputable def ratfunc.zero {K : Type u} [hring : comm_ring K] :

The zero rational function.

Equations
@[protected, instance]
noncomputable def ratfunc.has_zero {K : Type u} [hring : comm_ring K] :
Equations
theorem ratfunc.of_fraction_ring_zero {K : Type u} [hring : comm_ring K] :
@[protected]
noncomputable def ratfunc.add {K : Type u} [hring : comm_ring K] :

Equations
@[protected, instance]
noncomputable def ratfunc.has_add {K : Type u} [hring : comm_ring K] :
Equations
theorem ratfunc.of_fraction_ring_add {K : Type u} [hring : comm_ring K] (p q : fraction_ring (polynomial K)) :
@[protected]
noncomputable def ratfunc.sub {K : Type u} [hring : comm_ring K] :

Subtraction of rational functions.

Equations
@[protected, instance]
noncomputable def ratfunc.has_sub {K : Type u} [hring : comm_ring K] :
Equations
theorem ratfunc.of_fraction_ring_sub {K : Type u} [hring : comm_ring K] (p q : fraction_ring (polynomial K)) :
@[protected]
noncomputable def ratfunc.neg {K : Type u} [hring : comm_ring K] :

Additive inverse of a rational function.

Equations
@[protected, instance]
noncomputable def ratfunc.has_neg {K : Type u} [hring : comm_ring K] :
Equations
theorem ratfunc.of_fraction_ring_neg {K : Type u} [hring : comm_ring K] (p : fraction_ring (polynomial K)) :
@[protected]
noncomputable def ratfunc.one {K : Type u} [hring : comm_ring K] :

The multiplicative unit of rational functions.

Equations
@[protected, instance]
noncomputable def ratfunc.has_one {K : Type u} [hring : comm_ring K] :
Equations
theorem ratfunc.of_fraction_ring_one {K : Type u} [hring : comm_ring K] :
@[protected]
noncomputable def ratfunc.mul {K : Type u} [hring : comm_ring K] :

Multiplication of rational functions.

Equations
@[protected, instance]
noncomputable def ratfunc.has_mul {K : Type u} [hring : comm_ring K] :
Equations
theorem ratfunc.of_fraction_ring_mul {K : Type u} [hring : comm_ring K] (p q : fraction_ring (polynomial K)) :
@[protected]
noncomputable def ratfunc.div {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :

Division of rational functions.

Equations
@[protected, instance]
noncomputable def ratfunc.has_div {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :
Equations
theorem ratfunc.of_fraction_ring_div {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p q : fraction_ring (polynomial K)) :
@[protected]
noncomputable def ratfunc.inv {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :

Multiplicative inverse of a rational function.

Equations
@[protected, instance]
noncomputable def ratfunc.has_inv {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :
Equations
theorem ratfunc.of_fraction_ring_inv {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : fraction_ring (polynomial K)) :
theorem ratfunc.mul_inv_cancel {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {p : ratfunc K} (hp : p 0) :
p * p⁻¹ = 1
@[protected]
def ratfunc.smul {K : Type u} [hring : comm_ring K] {R : Type u_1} [ (fraction_ring (polynomial K))] :
R →

Scalar multiplication of rational functions.

Equations
@[protected, nolint, instance]
def ratfunc.has_scalar {K : Type u} [hring : comm_ring K] {R : Type u_1} [ (fraction_ring (polynomial K))] :
(ratfunc K)
Equations
theorem ratfunc.of_fraction_ring_smul {K : Type u} [hring : comm_ring K] {R : Type u_1} [ (fraction_ring (polynomial K))] (c : R) (p : fraction_ring (polynomial K)) :
theorem ratfunc.to_fraction_ring_smul {K : Type u} [hring : comm_ring K] {R : Type u_1} [ (fraction_ring (polynomial K))] (c : R) (p : ratfunc K) :
theorem ratfunc.smul_eq_C_smul {K : Type u} [hring : comm_ring K] (x : ratfunc K) (r : K) :
r x =
theorem ratfunc.mk_smul {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {R : Type u_1} [monoid R] [ (polynomial K)] [htower : (polynomial K)] (c : R) (p q : polynomial K) :
ratfunc.mk (c p) q = c q
@[protected, instance]
def ratfunc.is_scalar_tower {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {R : Type u_1} [monoid R] [ (polynomial K)] [htower : (polynomial K)] :
(ratfunc K)
@[protected, instance]
def ratfunc.subsingleton (K : Type u) [hring : comm_ring K] [subsingleton K] :
@[protected, instance]
noncomputable def ratfunc.inhabited (K : Type u) [hring : comm_ring K] :
Equations
@[protected, instance]
def ratfunc.nontrivial (K : Type u) [hring : comm_ring K] [nontrivial K] :
def ratfunc.to_fraction_ring_ring_equiv (K : Type u) [hring : comm_ring K] :

`ratfunc K` is isomorphic to the field of fractions of `polynomial K`, as rings.

This is an auxiliary definition; `simp`-normal form is `is_localization.alg_equiv`.

Equations
@[simp]
theorem ratfunc.to_fraction_ring_ring_equiv_apply (K : Type u) [hring : comm_ring K] (self : ratfunc K) :
meta def ratfunc.frac_tac  :

Solve equations for `ratfunc K` by working in `fraction_ring K[X]`.

meta def ratfunc.smul_tac  :

Solve equations for `ratfunc K` by applying `ratfunc.induction_on`.

@[protected, instance]
noncomputable def ratfunc.comm_ring (K : Type u) [hring : comm_ring K] :
Equations
noncomputable def ratfunc.map {R : Type u_3} {S : Type u_4} {F : Type u_5} [comm_ring R] [comm_ring S] [ (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
theorem ratfunc.map_apply_of_fraction_ring_mk {R : Type u_3} {S : Type u_4} {F : Type u_5} [comm_ring R] [comm_ring S] [ (polynomial S)] (φ : F) (hφ : ) (n : polynomial R) (d : ) :
theorem ratfunc.map_injective {R : Type u_3} {S : Type u_4} {F : Type u_5} [comm_ring R] [comm_ring S] [ (polynomial S)] (φ : F) (hφ : ) (hf : function.injective φ) :
noncomputable def ratfunc.map_ring_hom {R : Type u_3} {S : Type u_4} {F : Type u_5} [comm_ring R] [comm_ring S] [ (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
theorem ratfunc.coe_map_ring_hom_eq_coe_map {R : Type u_3} {S : Type u_4} {F : Type u_5} [comm_ring R] [comm_ring S] [ (polynomial R) (polynomial S)] (φ : F) (hφ : ) :
hφ) = hφ)
noncomputable def ratfunc.lift_monoid_with_zero_hom {G₀ : Type u_1} {R : Type u_3} [comm_ring R] (φ : →*₀ G₀) (hφ : ) :
→*₀ G₀

Lift an monoid with zero homomorphism `polynomial R →*₀ 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
theorem ratfunc.lift_monoid_with_zero_hom_apply_of_fraction_ring_mk {G₀ : Type u_1} {R : Type u_3} [comm_ring R] (φ : →*₀ G₀) (hφ : ) (n : polynomial R) (d : ) :
{to_fraction_ring := d} = φ n / φ d
theorem ratfunc.lift_monoid_with_zero_hom_injective {G₀ : Type u_1} {R : Type u_3} [comm_ring R] [nontrivial R] (φ : →*₀ G₀) (hφ : function.injective φ) (hφ' : := _) :
noncomputable def ratfunc.lift_ring_hom {L : Type u_2} {R : Type u_3} [field L] [comm_ring R] (φ : →+* L) (hφ : ) :

Lift an injective ring homomorphism `polynomial R →+* L` to a `ratfunc R →+* L` by mapping both the numerator and denominator and quotienting them. -

Equations
theorem ratfunc.lift_ring_hom_apply_of_fraction_ring_mk {L : Type u_2} {R : Type u_3} [field L] [comm_ring R] (φ : →+* L) (hφ : ) (n : polynomial R) (d : ) :
hφ) {to_fraction_ring := d} = φ n / φ d
theorem ratfunc.lift_ring_hom_injective {L : Type u_2} {R : Type u_3} [field L] [comm_ring R] [nontrivial R] (φ : →+* L) (hφ : function.injective φ) (hφ' : := _) :
@[protected, instance]
noncomputable def ratfunc.field (K : Type u) [hring : comm_ring K] [hdomain : is_domain K] :
Equations

### `ratfunc` as field of fractions of `polynomial`#

@[protected, instance]
noncomputable def ratfunc.algebra {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (R : Type u_1) [ (polynomial K)] :
(ratfunc K)
Equations
theorem ratfunc.mk_one {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (x : polynomial K) :
1 = (ratfunc K)) x
theorem ratfunc.of_fraction_ring_algebra_map {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (x : polynomial K) :
@[simp]
theorem ratfunc.mk_eq_div {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p q : polynomial K) :
q = (ratfunc K)) p / (ratfunc K)) q
@[simp]
theorem ratfunc.div_smul {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {R : Type u_1} [monoid R] [ (polynomial K)] [ (polynomial K)] (c : R) (p q : polynomial K) :
(ratfunc K)) (c p) / (ratfunc K)) q = c ( (ratfunc K)) p / (ratfunc K)) q)
theorem ratfunc.algebra_map_apply {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {R : Type u_1} [ (polynomial K)] (x : R) :
(ratfunc K)) x = (ratfunc K)) ( (polynomial K)) x) / (ratfunc K)) 1
theorem ratfunc.map_apply_div_ne_zero {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {R : Type u_1} {F : Type u_2} [comm_ring R] [is_domain R] [ (polynomial R)] (φ : F) (hφ : ) (p q : polynomial K) (hq : q 0) :
hφ) ( (ratfunc K)) p / (ratfunc K)) q) = (ratfunc R)) (φ p) / (ratfunc R)) (φ q)
@[simp]
theorem ratfunc.map_apply_div {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {R : Type u_1} {F : Type u_2} [comm_ring R] [is_domain R] [ (polynomial R)] (φ : F) (hφ : ) (p q : polynomial K) :
hφ) ( (ratfunc K)) p / (ratfunc K)) q) = (ratfunc R)) (φ p) / (ratfunc R)) (φ q)
@[simp]
theorem ratfunc.lift_monoid_with_zero_hom_apply_div {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {L : Type u_1} (φ : →*₀ L) (hφ : ) (p q : polynomial K) :
( (ratfunc K)) p / (ratfunc K)) q) = φ p / φ q
@[simp]
theorem ratfunc.lift_ring_hom_apply_div {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {L : Type u_1} [field L] (φ : →+* L) (hφ : ) (p q : polynomial K) :
hφ) ( (ratfunc K)) p / (ratfunc K)) q) = φ p / φ q
theorem ratfunc.of_fraction_ring_comp_algebra_map (K : Type u) [hring : comm_ring K] [hdomain : is_domain K] :
ratfunc.of_fraction_ring (fraction_ring (polynomial K))) = (ratfunc K))
theorem ratfunc.algebra_map_injective (K : Type u) [hring : comm_ring K] [hdomain : is_domain K] :
@[simp]
theorem ratfunc.algebra_map_eq_zero_iff (K : Type u) [hring : comm_ring K] [hdomain : is_domain K] {x : polynomial K} :
(ratfunc K)) x = 0 x = 0
theorem ratfunc.algebra_map_ne_zero {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {x : polynomial K} (hx : x 0) :
(ratfunc K)) x 0
noncomputable def ratfunc.map_alg_hom {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {R : Type u_2} {S : Type u_3} [comm_ring R] [is_domain R] [ (polynomial K)] [ (polynomial R)] (φ : →ₐ[S] ) (hφ : ) :

Lift an algebra homomorphism that maps polynomials `φ : polynomial K →ₐ[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
theorem ratfunc.coe_map_alg_hom_eq_coe_map {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {R : Type u_2} {S : Type u_3} [comm_ring R] [is_domain R] [ (polynomial K)] [ (polynomial R)] (φ : →ₐ[S] ) (hφ : ) :
hφ) = hφ)
noncomputable def ratfunc.lift_alg_hom {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {L : Type u_1} {S : Type u_3} [field L] [ (polynomial K)] [ L] (φ : →ₐ[S] L) (hφ : ) :

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

Equations
theorem ratfunc.lift_alg_hom_apply_of_fraction_ring_mk {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {L : Type u_1} {S : Type u_3} [field L] [ (polynomial K)] [ L] (φ : →ₐ[S] L) (hφ : ) (n : polynomial K) (d : ) :
hφ) {to_fraction_ring := d} = φ n / φ d
theorem ratfunc.lift_alg_hom_injective {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {L : Type u_1} {S : Type u_3} [field L] [ (polynomial K)] [ L] (φ : →ₐ[S] L) (hφ : function.injective φ) (hφ' : := _) :
@[simp]
theorem ratfunc.lift_alg_hom_apply_div {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {L : Type u_1} {S : Type u_3} [field L] [ (polynomial K)] [ L] (φ : →ₐ[S] L) (hφ : ) (p q : polynomial K) :
hφ) ( (ratfunc K)) p / (ratfunc K)) q) = φ p / φ q
@[protected, instance]
def ratfunc.is_fraction_ring (K : Type u) [hring : comm_ring K] [hdomain : is_domain K] :
(ratfunc K)

`ratfunc K` is the field of fractions of the polynomials over `K`.

@[simp]
theorem ratfunc.lift_on_div {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {P : Sort v} (p q : polynomial K) (f : → P) (f0 : ∀ (p : , f p 0 = f 0 1) (H' : ∀ {p q p' q' : , q 0q' 0p * q' = p' * qf p q = f p' q') (H : (∀ {p q p' q' : , q' p * q' = p' * qf p q = f p' q') := _) :
( (ratfunc K)) p / (ratfunc K)) q).lift_on f H = f p q
@[simp]
theorem ratfunc.lift_on'_div {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {P : Sort v} (p q : polynomial K) (f : → P) (f0 : ∀ (p : , f p 0 = f 0 1) (H : ∀ {p q a : , q 0a 0f (a * p) (a * q) = f p q) :
( (ratfunc K)) p / (ratfunc K)) q).lift_on' f H = f p q
@[protected]
theorem ratfunc.induction_on {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {P : → Prop} (x : ratfunc K) (f : ∀ (p q : , q 0P ( (ratfunc K)) p / (ratfunc K)) q)) :
P x

Induction principle for `ratfunc K`: if `f p q : P (p / q)` for all `p q : polynomial K`, 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.of_fraction_ring_mk' {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (x : polynomial K) (y : ) :
@[simp]
theorem ratfunc.of_fraction_ring_eq {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :
ratfunc.of_fraction_ring = (ratfunc K))
@[simp]
theorem ratfunc.to_fraction_ring_eq {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :
@[simp]
theorem ratfunc.to_fraction_ring_ring_equiv_symm_eq {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :

### Numerator and denominator #

noncomputable def ratfunc.num_denom {K : Type u} [hfield : field K] (x : ratfunc K) :

`ratfunc.num_denom` are numerator and denominator of a rational function over a field, normalized such that the denominator is monic.

Equations
@[simp]
theorem ratfunc.num_denom_div {K : Type u} [hfield : field K] (p : polynomial K) {q : polynomial K} (hq : q 0) :
noncomputable def ratfunc.num {K : Type u} [hfield : field K] (x : ratfunc K) :

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

Equations
@[simp]
theorem ratfunc.num_zero {K : Type u} [hfield : field K] :
0.num = 0
@[simp]
theorem ratfunc.num_div {K : Type u} [hfield : field K] (p q : polynomial K) :
( (ratfunc K)) p / (ratfunc K)) q).num = polynomial.C ((q / q).leading_coeff)⁻¹ * (p / q)
@[simp]
theorem ratfunc.num_one {K : Type u} [hfield : field K] :
1.num = 1
@[simp]
theorem ratfunc.num_algebra_map {K : Type u} [hfield : field K] (p : polynomial K) :
( (ratfunc K)) p).num = p
theorem ratfunc.num_div_dvd {K : Type u} [hfield : field K] (p : polynomial K) {q : polynomial K} (hq : q 0) :
( (ratfunc K)) p / (ratfunc K)) q).num p
@[simp]
theorem ratfunc.num_div_dvd' {K : Type u} [hfield : field K] (p : polynomial K) {q : polynomial K} (hq : q 0) :

A version of `num_div_dvd` with the LHS in simp normal form

noncomputable def ratfunc.denom {K : Type u} [hfield : field K] (x : ratfunc K) :

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

Equations
@[simp]
theorem ratfunc.denom_div {K : Type u} [hfield : field K] (p : polynomial K) {q : polynomial K} (hq : q 0) :
theorem ratfunc.monic_denom {K : Type u} [hfield : field K] (x : ratfunc K) :
theorem ratfunc.denom_ne_zero {K : Type u} [hfield : field K] (x : ratfunc K) :
@[simp]
theorem ratfunc.denom_zero {K : Type u} [hfield : field K] :
0.denom = 1
@[simp]
theorem ratfunc.denom_one {K : Type u} [hfield : field K] :
1.denom = 1
@[simp]
theorem ratfunc.denom_algebra_map {K : Type u} [hfield : field K] (p : polynomial K) :
( (ratfunc K)) p).denom = 1
@[simp]
theorem ratfunc.denom_div_dvd {K : Type u} [hfield : field K] (p q : polynomial K) :
( (ratfunc K)) p / (ratfunc K)) q).denom q
@[simp]
theorem ratfunc.num_div_denom {K : Type u} [hfield : field K] (x : ratfunc K) :
(ratfunc K)) x.num / (ratfunc K)) x.denom = x
@[simp]
theorem ratfunc.num_eq_zero_iff {K : Type u} [hfield : field K] {x : ratfunc K} :
x.num = 0 x = 0
theorem ratfunc.num_ne_zero {K : Type u} [hfield : field K] {x : ratfunc K} (hx : x 0) :
x.num 0
theorem ratfunc.num_mul_eq_mul_denom_iff {K : Type u} [hfield : field K] {x : ratfunc K} {p q : polynomial K} (hq : q 0) :
x.num * q = p * x.denom x = (ratfunc K)) p / (ratfunc K)) q
theorem ratfunc.num_denom_add {K : Type u} [hfield : field K] (x 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} [hfield : field K] (x : ratfunc K) :
(-x).num * x.denom = -x.num * (-x).denom
theorem ratfunc.num_denom_mul {K : Type u} [hfield : field K] (x y : ratfunc K) :
(x * y).num * (x.denom * y.denom) = x.num * y.num * (x * y).denom
theorem ratfunc.num_dvd {K : Type u} [hfield : field K] {x : ratfunc K} {p : polynomial K} (hp : p 0) :
x.num p ∃ (q : (hq : q 0), x = (ratfunc K)) p / (ratfunc K)) q
theorem ratfunc.denom_dvd {K : Type u} [hfield : field K] {x : ratfunc K} {q : polynomial K} (hq : q 0) :
x.denom q ∃ (p : , x = (ratfunc K)) p / (ratfunc K)) q
theorem ratfunc.num_mul_dvd {K : Type u} [hfield : field K] (x y : ratfunc K) :
(x * y).num x.num * y.num
theorem ratfunc.denom_mul_dvd {K : Type u} [hfield : field K] (x y : ratfunc K) :
(x * y).denom x.denom * y.denom
theorem ratfunc.denom_add_dvd {K : Type u} [hfield : field K] (x y : ratfunc K) :
(x + y).denom x.denom * y.denom
theorem ratfunc.map_denom_ne_zero {K : Type u} [hfield : field K] {L : Type u_1} {F : Type u_2} [has_zero L] [ (polynomial K) L] (φ : F) (hφ : function.injective φ) (f : ratfunc K) :
φ f.denom 0
theorem ratfunc.map_apply {K : Type u} [hfield : field K] {R : Type u_1} {F : Type u_2} [comm_ring R] [is_domain R] [ (polynomial R)] (φ : F) (hφ : ) (f : ratfunc K) :
hφ) f = (ratfunc R)) (φ f.num) / (ratfunc R)) (φ f.denom)
theorem ratfunc.lift_monoid_with_zero_hom_apply {K : Type u} [hfield : field K] {L : Type u_1} (φ : →*₀ L) (hφ : ) (f : ratfunc K) :
= φ f.num / φ f.denom
theorem ratfunc.lift_ring_hom_apply {K : Type u} [hfield : field K] {L : Type u_1} [field L] (φ : →+* L) (hφ : ) (f : ratfunc K) :
hφ) f = φ f.num / φ f.denom
theorem ratfunc.lift_alg_hom_apply {K : Type u} [hfield : field K] {L : Type u_1} {S : Type u_2} [field L] [ (polynomial K)] [ L] (φ : →ₐ[S] L) (hφ : ) (f : ratfunc K) :
hφ) f = φ f.num / φ f.denom
theorem ratfunc.num_mul_denom_add_denom_mul_num_ne_zero {K : Type u} [hfield : field K] {x y : ratfunc K} (hxy : x + y 0) :
x.num * y.denom + x.denom * y.num 0

### Polynomial structure: `C`, `X`, `eval`#

noncomputable def ratfunc.C {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :

`ratfunc.C a` is the constant rational function `a`.

Equations
@[simp]
theorem ratfunc.algebra_map_eq_C {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :
@[simp]
theorem ratfunc.algebra_map_C {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (a : K) :
(ratfunc K)) =
@[simp]
theorem ratfunc.algebra_map_comp_C {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :
theorem ratfunc.smul_eq_C_mul {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (r : K) (x : ratfunc K) :
r x = * x
noncomputable def ratfunc.X {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :

`ratfunc.X` is the polynomial variable (aka indeterminate).

Equations
@[simp]
theorem ratfunc.algebra_map_X {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :
@[simp]
theorem ratfunc.num_C {K : Type u} [hfield : field K] (c : K) :
@[simp]
theorem ratfunc.denom_C {K : Type u} [hfield : field K] (c : K) :
@[simp]
theorem ratfunc.num_X {K : Type u} [hfield : field K] :
@[simp]
theorem ratfunc.denom_X {K : Type u} [hfield : field K] :
theorem ratfunc.X_ne_zero {K : Type u} [hfield : field K] :
noncomputable def ratfunc.eval {K : Type u} [hfield : 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
theorem ratfunc.eval_eq_zero_of_eval₂_denom_eq_zero {K : Type u} [hfield : field K] {L : Type u_1} [field L] {f : K →+* L} {a : L} {x : ratfunc K} (h : x.denom = 0) :
a x = 0
theorem ratfunc.eval₂_denom_ne_zero {K : Type u} [hfield : field K] {L : Type u_1} [field L] {f : K →+* L} {a : L} {x : ratfunc K} (h : a x 0) :
x.denom 0
@[simp]
theorem ratfunc.eval_C {K : Type u} [hfield : field K] {L : Type u_1} [field L] (f : K →+* L) (a : L) {c : K} :
a (ratfunc.C c) = f c
@[simp]
theorem ratfunc.eval_X {K : Type u} [hfield : field K] {L : Type u_1} [field L] (f : K →+* L) (a : L) :
= a
@[simp]
theorem ratfunc.eval_zero {K : Type u} [hfield : field K] {L : Type u_1} [field L] (f : K →+* L) (a : L) :
a 0 = 0
@[simp]
theorem ratfunc.eval_one {K : Type u} [hfield : field K] {L : Type u_1} [field L] (f : K →+* L) (a : L) :
a 1 = 1
@[simp]
theorem ratfunc.eval_algebra_map {K : Type u} [hfield : field K] {L : Type u_1} [field L] (f : K →+* L) (a : L) {S : Type u_2} [ (polynomial K)] (p : S) :
a ( (ratfunc K)) p) = ( (polynomial K)) p)
theorem ratfunc.eval_add {K : Type u} [hfield : field K] {L : Type u_1} [field L] (f : K →+* L) (a : L) {x y : ratfunc K} (hx : x.denom 0) (hy : y.denom 0) :
a (x + y) = a x + 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} [hfield : field K] {L : Type u_1} [field L] (f : K →+* L) (a : L) {x y : ratfunc K} (hx : x.denom 0) (hy : y.denom 0) :
a (x * y) = a x * 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.

noncomputable def ratfunc.int_degree {K : Type u} [field K] (x : ratfunc K) :

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

Equations
@[simp]
theorem ratfunc.int_degree_zero {K : Type u} [field K] :
@[simp]
theorem ratfunc.int_degree_one {K : Type u} [field K] :
@[simp]
theorem ratfunc.int_degree_C {K : Type u} [field K] (k : K) :
@[simp]
theorem ratfunc.int_degree_X {K : Type u} [field K] :
@[simp]
theorem ratfunc.int_degree_polynomial {K : Type u} [field K] {p : polynomial K} :
theorem ratfunc.int_degree_mul {K : Type u} [field K] {x y : ratfunc K} (hx : x 0) (hy : y 0) :
(x * y).int_degree =
@[simp]
theorem ratfunc.int_degree_neg {K : Type u} [field K] (x : ratfunc K) :
theorem ratfunc.int_degree_add {K : Type u} [field K] {x y : ratfunc K} (hxy : x + y 0) :
theorem ratfunc.int_degree_add_le {K : Type u} [field K] {x y : ratfunc K} (hy : y 0) (hxy : x + y 0) :
noncomputable def ratfunc.coe_alg_hom (F : Type u) [field F] :

The coercion `ratfunc F → laurent_series F` as bundled alg hom.

Equations
@[protected, instance]
noncomputable def ratfunc.coe_to_laurent_series {F : Type u} [field F] :
Equations
theorem ratfunc.coe_def {F : Type u} [field F] (f : ratfunc F) :
f = f
theorem ratfunc.coe_num_denom {F : Type u} [field F] (f : ratfunc F) :
f = (f.num) / (f.denom)
theorem ratfunc.coe_injective {F : Type u} [field F] :
@[simp, norm_cast]
theorem ratfunc.coe_apply {F : Type u} [field F] (f : ratfunc F) :
f = f
@[simp, norm_cast]
theorem ratfunc.coe_zero {F : Type u} [field F] :
0 = 0
@[simp, norm_cast]
theorem ratfunc.coe_one {F : Type u} [field F] :
1 = 1
@[simp, norm_cast]
theorem ratfunc.coe_add {F : Type u} [field F] (f g : ratfunc F) :
(f + g) = f + g
@[simp, norm_cast]
theorem ratfunc.coe_mul {F : Type u} [field F] (f g : ratfunc F) :
(f * g) = f * g
@[simp, norm_cast]
theorem ratfunc.coe_div {F : Type u} [field F] (f g : ratfunc F) :
(f / g) = f / g
@[simp, norm_cast]
theorem ratfunc.coe_C {F : Type u} [field F] (r : F) :
@[simp, norm_cast]
theorem ratfunc.coe_smul {F : Type u} [field F] (f : ratfunc F) (r : F) :
(r f) = r f
@[simp, norm_cast]
theorem ratfunc.coe_X {F : Type u} [field F] :
@[protected, instance]
noncomputable def ratfunc.laurent_series.algebra {F : Type u} [field F] :
Equations
theorem ratfunc.algebra_map_apply_div {F : Type u} [field F] (p q : polynomial F) :
@[protected, instance]