mathlib documentation

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:

Working with rational functions as fractions:

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:

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

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.

Constructing ratfuncs and their induction principles #

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

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 : K[X]) :
theorem ratfunc.mk_zero {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : K[X]) :
theorem ratfunc.mk_coe_def {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : K[X]) (q : K[X]) :
theorem ratfunc.mk_def_of_mem {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : K[X]) {q : K[X]} (hq : q K[X]) :
theorem ratfunc.mk_def_of_ne {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : K[X]) {q : K[X]} (hq : q 0) :
theorem ratfunc.mk_eq_localization_mk {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : K[X]) {q : K[X]} (hq : q 0) :
theorem ratfunc.mk_one' {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : K[X]) :
theorem ratfunc.mk_eq_mk {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {p q p' q' : K[X]} (hq : q 0) (hq' : q' 0) :
ratfunc.mk p q = ratfunc.mk p' 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 : K[X]) (f : K[X]K[X] → P) (f0 : ∀ (p : K[X]), f p 0 = f 0 1) (H' : ∀ {p q p' q' : K[X]}, q 0q' 0p * q' = p' * qf p q = f p' q') (H : (∀ {p q p' q' : K[X]}, q K[X]q' K[X]p * q' = p' * qf p q = f p' q') := _) :
(ratfunc.mk p 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 : K[X]K[X] → P} (H : ∀ {p q a : K[X]}, q 0a 0f (a * p) (a * q) = f p q) ⦃p q p' q' : K[X] (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 : K[X]K[X] → P) (H : ∀ {p q a : K[X]}, 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 : K[X]) (f : K[X]K[X] → P) (f0 : ∀ (p : K[X]), f p 0 = f 0 1) (H : ∀ {p q a : K[X]}, q 0a 0f (a * p) (a * q) = f p q) :
(ratfunc.mk p 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 : ratfunc K → Prop} (x : ratfunc K) (f : ∀ (p q : K[X]), 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 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] :
ratfunc Kratfunc Kratfunc K

Addition of rational functions.

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 K[X]) :
@[protected]
noncomputable def ratfunc.sub {K : Type u} [hring : comm_ring K] :
ratfunc Kratfunc Kratfunc 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 K[X]) :
@[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 K[X]) :
@[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] :
ratfunc Kratfunc Kratfunc 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 K[X]) :
@[protected]
noncomputable def ratfunc.div {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :
ratfunc Kratfunc Kratfunc 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 K[X]) :
@[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 K[X]) :
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} [has_scalar R (fraction_ring K[X])] :
R → ratfunc Kratfunc K

Scalar multiplication of rational functions.

Equations
@[protected, instance]
def ratfunc.has_scalar {K : Type u} [hring : comm_ring K] {R : Type u_1} [has_scalar R (fraction_ring K[X])] :
Equations
theorem ratfunc.of_fraction_ring_smul {K : Type u} [hring : comm_ring K] {R : Type u_1} [has_scalar R (fraction_ring K[X])] (c : R) (p : fraction_ring K[X]) :
theorem ratfunc.to_fraction_ring_smul {K : Type u} [hring : comm_ring K] {R : Type u_1} [has_scalar R (fraction_ring K[X])] (c : R) (p : ratfunc K) :
theorem ratfunc.smul_eq_C_smul {K : Type u} [hring : comm_ring K] (x : ratfunc K) (r : K) :
theorem ratfunc.mk_smul {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {R : Type u_1} [monoid R] [distrib_mul_action R K[X]] [htower : is_scalar_tower R K[X] K[X]] (c : R) (p q : K[X]) :
ratfunc.mk (c p) q = c ratfunc.mk p 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] [distrib_mul_action R K[X]] [htower : is_scalar_tower R K[X] K[X]] :
@[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] :

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

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

Solve equations for ratfunc K by applying ratfunc.induction_on.

noncomputable def ratfunc.map {R : Type u_3} {S : Type u_4} {F : Type u_5} [comm_ring R] [comm_ring S] [monoid_hom_class F R[X] S[X]] (φ : F) (hφ : R[X] submonoid.comap φ S[X]) :

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] [monoid_hom_class F R[X] S[X]] (φ : F) (hφ : R[X] submonoid.comap φ S[X]) (n : R[X]) (d : R[X]) :
theorem ratfunc.map_injective {R : Type u_3} {S : Type u_4} {F : Type u_5} [comm_ring R] [comm_ring S] [monoid_hom_class F R[X] S[X]] (φ : F) (hφ : R[X] submonoid.comap φ S[X]) (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] [ring_hom_class F R[X] S[X]] (φ : F) (hφ : R[X] submonoid.comap φ S[X]) :

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] [ring_hom_class F R[X] S[X]] (φ : F) (hφ : R[X] submonoid.comap φ S[X]) :
noncomputable def ratfunc.lift_monoid_with_zero_hom {G₀ : Type u_1} {R : Type u_3} [comm_group_with_zero G₀] [comm_ring R] (φ : R[X] →*₀ G₀) (hφ : R[X] submonoid.comap φ 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
noncomputable def ratfunc.lift_ring_hom {L : Type u_2} {R : Type u_3} [field L] [comm_ring R] (φ : R[X] →+* L) (hφ : R[X] submonoid.comap φ L) :

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] (φ : R[X] →+* L) (hφ : R[X] submonoid.comap φ L) (n : R[X]) (d : R[X]) :
theorem ratfunc.lift_ring_hom_injective {L : Type u_2} {R : Type u_3} [field L] [comm_ring R] [nontrivial R] (φ : R[X] →+* L) (hφ : function.injective φ) (hφ' : R[X] submonoid.comap φ L := _) :

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) [comm_semiring R] [algebra R K[X]] :
Equations
theorem ratfunc.mk_one {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (x : K[X]) :
theorem ratfunc.of_fraction_ring_algebra_map {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (x : K[X]) :
@[simp]
theorem ratfunc.mk_eq_div {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p q : K[X]) :
@[simp]
theorem ratfunc.div_smul {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {R : Type u_1} [monoid R] [distrib_mul_action R K[X]] [is_scalar_tower R K[X] K[X]] (c : R) (p q : K[X]) :
theorem ratfunc.algebra_map_apply {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {R : Type u_1} [comm_semiring R] [algebra R K[X]] (x : R) :
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] [monoid_hom_class F K[X] R[X]] (φ : F) (hφ : K[X] submonoid.comap φ R[X]) (p q : K[X]) (hq : q 0) :
@[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] [monoid_with_zero_hom_class F K[X] R[X]] (φ : F) (hφ : K[X] submonoid.comap φ R[X]) (p q : K[X]) :
@[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} [comm_group_with_zero L] (φ : K[X] →*₀ L) (hφ : K[X] submonoid.comap φ L) (p q : K[X]) :
@[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] (φ : K[X] →+* L) (hφ : K[X] submonoid.comap φ L) (p q : K[X]) :
theorem ratfunc.of_fraction_ring_comp_algebra_map (K : Type u) [hring : comm_ring K] [hdomain : is_domain K] :
ratfunc.of_fraction_ring (algebra_map K[X] (fraction_ring K[X])) = (algebra_map K[X] (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 : K[X]} :
(algebra_map K[X] (ratfunc K)) x = 0 x = 0
theorem ratfunc.algebra_map_ne_zero {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {x : K[X]} (hx : 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] [comm_semiring S] [algebra S K[X]] [algebra S R[X]] (φ : K[X] →ₐ[S] R[X]) (hφ : K[X] submonoid.comap φ R[X]) :

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] [comm_semiring S] [algebra S K[X]] [algebra S R[X]] (φ : K[X] →ₐ[S] R[X]) (hφ : K[X] submonoid.comap φ R[X]) :
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] [comm_semiring S] [algebra S K[X]] [algebra S L] (φ : K[X] →ₐ[S] L) (hφ : K[X] submonoid.comap φ L) :

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] [comm_semiring S] [algebra S K[X]] [algebra S L] (φ : K[X] →ₐ[S] L) (hφ : K[X] submonoid.comap φ L) (n : K[X]) (d : K[X]) :
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] [comm_semiring S] [algebra S K[X]] [algebra S L] (φ : K[X] →ₐ[S] L) (hφ : function.injective φ) (hφ' : K[X] submonoid.comap φ L := _) :
@[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] [comm_semiring S] [algebra S K[X]] [algebra S L] (φ : K[X] →ₐ[S] L) (hφ : K[X] submonoid.comap φ L) (p q : K[X]) :
@[protected, instance]
def ratfunc.is_fraction_ring (K : Type u) [hring : comm_ring K] [hdomain : is_domain 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 : K[X]) (f : K[X]K[X] → P) (f0 : ∀ (p : K[X]), f p 0 = f 0 1) (H' : ∀ {p q p' q' : K[X]}, q 0q' 0p * q' = p' * qf p q = f p' q') (H : (∀ {p q p' q' : K[X]}, q K[X]q' K[X]p * q' = p' * qf p q = f p' q') := _) :
((algebra_map K[X] (ratfunc K)) p / (algebra_map K[X] (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 : K[X]) (f : K[X]K[X] → P) (f0 : ∀ (p : K[X]), f p 0 = f 0 1) (H : ∀ {p q a : K[X]}, q 0a 0f (a * p) (a * q) = f p q) :
@[protected]
theorem ratfunc.induction_on {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {P : ratfunc K → Prop} (x : ratfunc K) (f : ∀ (p q : K[X]), q 0P ((algebra_map K[X] (ratfunc K)) p / (algebra_map K[X] (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 : K[X]) (y : K[X]) :
@[simp]
theorem ratfunc.of_fraction_ring_eq {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :
ratfunc.of_fraction_ring = (is_localization.alg_equiv K[X] (fraction_ring K[X]) (ratfunc 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 : K[X]) {q : K[X]} (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 : K[X]) :
@[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 : K[X]) :
theorem ratfunc.num_div_dvd {K : Type u} [hfield : field K] (p : K[X]) {q : K[X]} (hq : q 0) :
@[simp]
theorem ratfunc.num_div_dvd' {K : Type u} [hfield : field K] (p : K[X]) {q : K[X]} (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 : K[X]) {q : K[X]} (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 : K[X]) :
@[simp]
theorem ratfunc.denom_div_dvd {K : Type u} [hfield : field K] (p q : K[X]) :
@[simp]
theorem ratfunc.num_div_denom {K : Type u} [hfield : field K] (x : ratfunc K) :
@[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 : K[X]} (hq : q 0) :
(x.num) * q = p * x.denom x = (algebra_map K[X] (ratfunc K)) p / (algebra_map K[X] (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 : K[X]} (hp : p 0) :
x.num p ∃ (q : K[X]) (hq : q 0), x = (algebra_map K[X] (ratfunc K)) p / (algebra_map K[X] (ratfunc K)) q
theorem ratfunc.denom_dvd {K : Type u} [hfield : field K] {x : ratfunc K} {q : K[X]} (hq : q 0) :
x.denom q ∃ (p : K[X]), x = (algebra_map K[X] (ratfunc K)) p / (algebra_map K[X] (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] [zero_hom_class F K[X] 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] [monoid_hom_class F K[X] R[X]] (φ : F) (hφ : K[X] submonoid.comap φ R[X]) (f : ratfunc K) :
theorem ratfunc.lift_monoid_with_zero_hom_apply {K : Type u} [hfield : field K] {L : Type u_1} [comm_group_with_zero L] (φ : K[X] →*₀ L) (hφ : K[X] submonoid.comap φ L) (f : ratfunc K) :
theorem ratfunc.lift_ring_hom_apply {K : Type u} [hfield : field K] {L : Type u_1} [field L] (φ : K[X] →+* L) (hφ : K[X] submonoid.comap φ L) (f : ratfunc K) :
theorem ratfunc.lift_alg_hom_apply {K : Type u} [hfield : field K] {L : Type u_1} {S : Type u_2} [field L] [comm_semiring S] [algebra S K[X]] [algebra S L] (φ : K[X] →ₐ[S] L) (hφ : K[X] submonoid.comap φ L) (f : ratfunc K) :
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) :
@[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 = (ratfunc.C r) * 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 : polynomial.eval₂ f a x.denom = 0) :
ratfunc.eval f 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 : ratfunc.eval f a x 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} :
@[simp]
theorem ratfunc.eval_X {K : Type u} [hfield : field K] {L : Type u_1} [field L] (f : K →+* L) (a : L) :
@[simp]
theorem ratfunc.eval_zero {K : Type u} [hfield : 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} [hfield : field K] {L : Type u_1} [field L] (f : K →+* L) (a : L) :
ratfunc.eval f 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} [comm_semiring S] [algebra S K[X]] (p : S) :
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 : polynomial.eval₂ f a x.denom 0) (hy : polynomial.eval₂ f a y.denom 0) :
ratfunc.eval f a (x + y) = ratfunc.eval f a x + ratfunc.eval f a y

eval is an additive homomorphism except when a denominator evaluates to 0.

Counterexample: eval _ 1 (X / (X-1)) + eval _ 1 (-1 / (X-1)) = 0 ... ≠ 1 = eval _ 1 ((X-1) / (X-1)).

See also ratfunc.eval₂_denom_ne_zero to make the hypotheses simpler but less general.

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 : polynomial.eval₂ f a x.denom 0) (hy : polynomial.eval₂ f a y.denom 0) :
ratfunc.eval f a (x * y) = (ratfunc.eval f a x) * ratfunc.eval f a y

eval is a multiplicative homomorphism except when a denominator evaluates to 0.

Counterexample: eval _ 0 X * eval _ 0 (1/X) = 0 ≠ 1 = eval _ 0 1 = eval _ 0 (X * 1/X).

See also ratfunc.eval₂_denom_ne_zero to make the hypotheses simpler but less general.

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 : K[X]} :
theorem ratfunc.int_degree_mul {K : Type u} [field K] {x y : ratfunc K} (hx : x 0) (hy : y 0) :
@[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) :
(x + y).int_degree = (((x.num) * y.denom + (x.denom) * y.num).nat_degree) - (((x.denom) * y.denom).nat_degree)
theorem ratfunc.nat_degree_num_mul_right_sub_nat_degree_denom_mul_left_eq_int_degree {K : Type u} [field K] {x : ratfunc K} (hx : x 0) {s : K[X]} (hs : s 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) :
theorem ratfunc.coe_num_denom {F : Type u} [field F] (f : ratfunc F) :
f = (f.num) / (f.denom)
@[simp, norm_cast]
theorem ratfunc.coe_apply {F : Type u} [field F] (f : ratfunc 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
@[protected, instance]