mathlib3 documentation

field_theory.ratfunc

The field of rational functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definitions #

Working with rational functions as polynomials:

Working with rational functions as fractions:

Embedding of rational functions into Laurent series, provided as a coercion, utilizing the underlying ratfunc.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) [comm_ring K] :

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 K[X], especially fraction_ring K[X], are given by is_localization.algebra_equiv.

Instances for ratfunc

Constructing ratfuncs and their induction principles #

theorem ratfunc.of_fraction_ring_injective {K : Type u} [comm_ring K] :
function.injective ratfunc.of_fraction_ring
@[protected, irreducible]
noncomputable def ratfunc.lift_on {K : Type u} [comm_ring K] {P : Sort v} (x : ratfunc K) (f : polynomial K polynomial K P) (H : {p q p' q' : polynomial K}, q non_zero_divisors (polynomial K) q' non_zero_divisors (polynomial K) q' * p = q * p' f p q = f p' q') :
P

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

If considering K as an integral domain, this is the same as saying that we construct a value of P for such elements of ratfunc K by setting 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} [comm_ring K] {P : Sort v} (n : polynomial K) (d : (non_zero_divisors (polynomial K))) (f : polynomial K polynomial K P) (H : {p q p' q' : polynomial K}, q non_zero_divisors (polynomial K) q' non_zero_divisors (polynomial K) q' * p = q * p' f p q = f p' q') :
theorem ratfunc.lift_on_condition_of_lift_on'_condition {K : Type u} [comm_ring K] {P : Sort v} {f : polynomial K polynomial K P} (H : {p q a : polynomial K}, q 0 a 0 f (a * p) (a * q) = f p q) ⦃p q p' q' : polynomial K⦄ (hq : q 0) (hq' : q' 0) (h : q' * p = q * p') :
f p q = f p' q'
@[protected, irreducible]
noncomputable def ratfunc.mk {K : Type u} [comm_ring K] [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_zero {K : Type u} [comm_ring K] [is_domain K] (p : polynomial K) :
theorem ratfunc.mk_eq_localization_mk {K : Type u} [comm_ring K] [is_domain K] (p : polynomial K) {q : polynomial K} (hq : q 0) :
theorem ratfunc.mk_eq_mk {K : Type u} [comm_ring K] [is_domain K] {p q p' q' : polynomial K} (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} [comm_ring K] [is_domain K] {P : Sort v} (p q : polynomial K) (f : polynomial K polynomial K P) (f0 : (p : polynomial K), f p 0 = f 0 1) (H' : {p q p' q' : polynomial K}, q 0 q' 0 q' * p = q * p' f p q = f p' q') (H : ( {p q p' q' : polynomial K}, q non_zero_divisors (polynomial K) q' non_zero_divisors (polynomial K) q' * p = q * p' f p q = f p' q') := _) :
(ratfunc.mk p q).lift_on f H = f p q
@[protected, irreducible]
noncomputable def ratfunc.lift_on' {K : Type u} [comm_ring K] [is_domain K] {P : Sort v} (x : ratfunc K) (f : polynomial K polynomial K P) (H : {p q a : polynomial K}, q 0 a 0 f (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} [comm_ring K] [is_domain K] {P : Sort v} (p q : polynomial K) (f : polynomial K polynomial K P) (f0 : (p : polynomial K), f p 0 = f 0 1) (H : {p q a : polynomial K}, q 0 a 0 f (a * p) (a * q) = f p q) :
(ratfunc.mk p q).lift_on' f H = f p q
@[protected, irreducible]
theorem ratfunc.induction_on' {K : Type u} [comm_ring K] [is_domain K] {P : ratfunc K Prop} (x : ratfunc K) (f : (p q : polynomial K), q 0 P (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, irreducible]
noncomputable def ratfunc.zero {K : Type u} [comm_ring K] :

The zero rational function.

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

Addition of rational functions.

Equations
@[protected, instance]
noncomputable def ratfunc.has_add {K : Type u} [comm_ring K] :
Equations
@[protected, irreducible]
noncomputable def ratfunc.sub {K : Type u} [comm_ring K] :

Subtraction of rational functions.

Equations
@[protected, instance]
noncomputable def ratfunc.has_sub {K : Type u} [comm_ring K] :
Equations
@[protected, irreducible]
noncomputable def ratfunc.neg {K : Type u} [comm_ring K] :

Additive inverse of a rational function.

Equations
@[protected, instance]
noncomputable def ratfunc.has_neg {K : Type u} [comm_ring K] :
Equations
@[protected, irreducible]
noncomputable def ratfunc.one {K : Type u} [comm_ring K] :

The multiplicative unit of rational functions.

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

Multiplication of rational functions.

Equations
@[protected, instance]
noncomputable def ratfunc.has_mul {K : Type u} [comm_ring K] :
Equations
@[protected, irreducible]
noncomputable def ratfunc.div {K : Type u} [comm_ring K] [is_domain K] :

Division of rational functions.

Equations
@[protected, instance]
noncomputable def ratfunc.has_div {K : Type u} [comm_ring K] [is_domain K] :
Equations
@[protected, irreducible]
noncomputable def ratfunc.inv {K : Type u} [comm_ring K] [is_domain K] :

Multiplicative inverse of a rational function.

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

Scalar multiplication of rational functions.

Equations
@[protected, nolint, instance]
def ratfunc.has_smul {K : Type u} [comm_ring K] {R : Type u_1} [has_smul R (fraction_ring (polynomial K))] :
Equations
theorem ratfunc.smul_eq_C_smul {K : Type u} [comm_ring K] (x : ratfunc K) (r : K) :
theorem ratfunc.mk_smul {K : Type u} [comm_ring K] {R : Type u_1} [is_domain K] [monoid R] [distrib_mul_action R (polynomial K)] [is_scalar_tower R (polynomial K) (polynomial K)] (c : R) (p q : polynomial K) :
ratfunc.mk (c p) q = c ratfunc.mk p q
@[protected, instance]
@[protected, instance]
@[protected, instance]
noncomputable def ratfunc.inhabited (K : Type u) [comm_ring K] :
Equations
@[protected, instance]

ratfunc K is isomorphic to the field of fractions of K[X], 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.

@[protected, instance]
noncomputable def ratfunc.comm_ring (K : Type u) [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] [monoid_hom_class F (polynomial R) (polynomial S)] (φ : F) (hφ : non_zero_divisors (polynomial R) submonoid.comap φ (non_zero_divisors (polynomial S))) :

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
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 (polynomial R) (polynomial S)] (φ : F) (hφ : non_zero_divisors (polynomial R) submonoid.comap φ (non_zero_divisors (polynomial S))) :

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
noncomputable def ratfunc.lift_monoid_with_zero_hom {G₀ : Type u_1} {R : Type u_3} [comm_group_with_zero G₀] [comm_ring R] (φ : polynomial R →*₀ G₀) (hφ : non_zero_divisors (polynomial R) submonoid.comap φ (non_zero_divisors G₀)) :

Lift an 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
noncomputable def ratfunc.lift_ring_hom {L : Type u_2} {R : Type u_3} [field L] [comm_ring R] (φ : polynomial R →+* L) (hφ : non_zero_divisors (polynomial R) submonoid.comap φ (non_zero_divisors L)) :

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

Equations
@[protected, instance]
noncomputable def ratfunc.field (K : Type u) [comm_ring K] [is_domain K] :
Equations

ratfunc as field of fractions of polynomial #

@[protected, instance]
noncomputable def ratfunc.algebra (K : Type u) [comm_ring K] [is_domain K] (R : Type u_1) [comm_semiring R] [algebra R (polynomial K)] :
Equations
theorem ratfunc.mk_one {K : Type u} [comm_ring K] [is_domain K] (x : polynomial K) :
@[simp]
@[simp]
@[simp]
theorem ratfunc.algebra_map_ne_zero {K : Type u} [comm_ring K] [is_domain 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
noncomputable def ratfunc.lift_alg_hom {K : Type u} [comm_ring K] [is_domain K] {L : Type u_1} {S : Type u_3} [field L] [comm_semiring S] [algebra S (polynomial K)] [algebra S L] (φ : polynomial K →ₐ[S] L) (hφ : non_zero_divisors (polynomial K) submonoid.comap φ (non_zero_divisors L)) :

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
@[protected, instance]

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

@[simp]
theorem ratfunc.lift_on_div {K : Type u} [comm_ring K] [is_domain K] {P : Sort v} (p q : polynomial K) (f : polynomial K polynomial K P) (f0 : (p : polynomial K), f p 0 = f 0 1) (H' : {p q p' q' : polynomial K}, q 0 q' 0 q' * p = q * p' f p q = f p' q') (H : ( {p q p' q' : polynomial K}, q non_zero_divisors (polynomial K) q' non_zero_divisors (polynomial K) q' * p = q * p' f p q = f p' q') := _) :
@[simp]
theorem ratfunc.lift_on'_div {K : Type u} [comm_ring K] [is_domain K] {P : Sort v} (p q : polynomial K) (f : polynomial K polynomial K P) (f0 : (p : polynomial K), f p 0 = f 0 1) (H : {p q a : polynomial K}, q 0 a 0 f (a * p) (a * q) = f p q) :
@[protected]
theorem ratfunc.induction_on {K : Type u} [comm_ring K] [is_domain K] {P : ratfunc K Prop} (x : ratfunc K) (f : (p q : polynomial K), q 0 P ((algebra_map (polynomial K) (ratfunc K)) p / (algebra_map (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.

Numerator and denominator #

noncomputable def ratfunc.num_denom {K : Type u} [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
noncomputable 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
@[simp]
theorem ratfunc.num_zero {K : Type u} [field K] :
0.num = 0
@[simp]
theorem ratfunc.num_one {K : Type u} [field K] :
1.num = 1
@[simp]
theorem ratfunc.num_algebra_map {K : Type u} [field K] (p : polynomial K) :
theorem ratfunc.num_div_dvd {K : Type u} [field K] (p : polynomial K) {q : polynomial K} (hq : q 0) :
@[simp]
theorem ratfunc.num_div_dvd' {K : Type u} [field K] (p : polynomial K) {q : polynomial K} (hq : q 0) :

A version of num_div_dvd with the LHS in simp normal form

noncomputable 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
@[simp]
theorem ratfunc.monic_denom {K : Type u} [field K] (x : ratfunc K) :
theorem ratfunc.denom_ne_zero {K : Type u} [field K] (x : ratfunc K) :
@[simp]
theorem ratfunc.denom_zero {K : Type u} [field K] :
0.denom = 1
@[simp]
theorem ratfunc.denom_one {K : Type u} [field K] :
1.denom = 1
@[simp]
theorem ratfunc.denom_algebra_map {K : Type u} [field K] (p : polynomial K) :
@[simp]
theorem ratfunc.denom_div_dvd {K : Type u} [field K] (p q : polynomial K) :
@[simp]
@[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 q : polynomial K} (hq : q 0) :
theorem ratfunc.num_denom_add {K : Type u} [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} [field K] (x : ratfunc K) :
(-x).num * x.denom = -x.num * (-x).denom
theorem ratfunc.num_denom_mul {K : Type u} [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} [field K] {x : ratfunc K} {p : polynomial K} (hp : p 0) :
x.num p (q : polynomial K) (hq : q 0), x = (algebra_map (polynomial K) (ratfunc K)) p / (algebra_map (polynomial K) (ratfunc K)) q
theorem ratfunc.denom_dvd {K : Type u} [field K] {x : ratfunc K} {q : polynomial K} (hq : q 0) :
theorem ratfunc.num_mul_dvd {K : Type u} [field K] (x y : ratfunc K) :
(x * y).num x.num * y.num
theorem ratfunc.denom_mul_dvd {K : Type u} [field K] (x y : ratfunc K) :
(x * y).denom x.denom * y.denom
theorem ratfunc.denom_add_dvd {K : Type u} [field K] (x 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} [has_zero L] [zero_hom_class F (polynomial K) L] (φ : F) (hφ : function.injective φ) (f : ratfunc K) :
φ f.denom 0
theorem ratfunc.lift_alg_hom_apply {K : Type u} [field K] {L : Type u_1} {S : Type u_2} [field L] [comm_semiring S] [algebra S (polynomial K)] [algebra S L] (φ : polynomial K →ₐ[S] L) (hφ : non_zero_divisors (polynomial K) submonoid.comap φ (non_zero_divisors L)) (f : ratfunc K) :
theorem ratfunc.num_mul_denom_add_denom_mul_num_ne_zero {K : Type u} [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} [comm_ring K] [is_domain K] :

ratfunc.C a is the constant rational function a.

Equations
theorem ratfunc.smul_eq_C_mul {K : Type u} [comm_ring K] [is_domain K] (r : K) (x : ratfunc K) :
noncomputable def ratfunc.X {K : Type u} [comm_ring K] [is_domain K] :

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

Equations
@[simp]
theorem ratfunc.num_C {K : Type u} [field K] (c : K) :
@[simp]
theorem ratfunc.denom_C {K : Type u} [field K] (c : K) :
@[simp]
@[simp]
theorem ratfunc.denom_X {K : Type u} [field K] :
theorem ratfunc.X_ne_zero {K : Type u} [field K] :
noncomputable def ratfunc.eval {K : Type u} [field K] {L : Type u_1} [field L] (f : K →+* L) (a : L) (p : ratfunc K) :
L

Evaluate a rational function p given a ring hom f from the scalar field to the target and a value x for the variable in the target.

Fractions are reduced by clearing common denominators before evaluating: eval id 1 ((X^2 - 1) / (X - 1)) = eval id 1 (X + 1) = 2, not 0 / 0 = 0.

Equations
theorem ratfunc.eval_eq_zero_of_eval₂_denom_eq_zero {K : Type u} [field K] {L : Type u_1} [field L] {f : K →+* L} {a : L} {x : ratfunc K} (h : polynomial.eval₂ f a x.denom = 0) :
ratfunc.eval f a x = 0
theorem ratfunc.eval₂_denom_ne_zero {K : Type u} [field K] {L : Type u_1} [field L] {f : K →+* L} {a : L} {x : ratfunc K} (h : ratfunc.eval f a x 0) :
@[simp]
theorem ratfunc.eval_C {K : Type u} [field K] {L : Type u_1} [field L] (f : K →+* L) (a : L) {c : K} :
@[simp]
theorem ratfunc.eval_X {K : Type u} [field K] {L : Type u_1} [field L] (f : K →+* L) (a : L) :
@[simp]
theorem ratfunc.eval_zero {K : Type u} [field K] {L : Type u_1} [field L] (f : K →+* L) (a : L) :
ratfunc.eval f a 0 = 0
@[simp]
theorem ratfunc.eval_one {K : Type u} [field K] {L : Type u_1} [field L] (f : K →+* L) (a : L) :
ratfunc.eval f a 1 = 1
@[simp]
theorem ratfunc.eval_algebra_map {K : Type u} [field K] {L : Type u_1} [field L] (f : K →+* L) (a : L) {S : Type u_2} [comm_semiring S] [algebra S (polynomial K)] (p : S) :
theorem ratfunc.eval_add {K : Type u} [field K] {L : Type u_1} [field L] (f : K →+* L) (a : L) {x 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} [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_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) :
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_sub {F : Type u} [field F] (f g : ratfunc F) :
(f - g) = f - g
@[simp, norm_cast]
theorem ratfunc.coe_neg {F : Type u} [field F] (f : ratfunc F) :
@[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_pow {F : Type u} [field F] (f : ratfunc F) (n : ) :
(f ^ n) = f ^ n
@[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]