# 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]`

source
@[irreducible]
def RatFunc.zero {K : Type u_1} [CommRing K] :
RatFunc K

The zero rational function.

Equations

- RatFunc.zero = { toFractionRing := 0 }

Instances For

source
theorem RatFunc.zero_def {K : Type u_1} [CommRing K] :
RatFunc.zero = { toFractionRing := 0 }
source
instance RatFunc.instZero {K : Type u} [CommRing K] :
Zero (RatFunc K)
Equations

- RatFunc.instZero = { zero := RatFunc.zero }

source
theorem RatFunc.ofFractionRing_zero {K : Type u} [CommRing K] :
{ toFractionRing := 0 } = 0
source
theorem RatFunc.add_def {K : Type u_1} [CommRing K] (x✝ x✝¹ : RatFunc K) :
x✝.add x✝¹ = match x✝, x✝¹ with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p + q }
source
@[irreducible]
def RatFunc.add {K : Type u_1} [CommRing K] :
RatFunc K → RatFunc K → RatFunc K

Addition of rational functions.

Equations

- x✝¹.add x✝ = match x✝¹, x✝ with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p + q }

Instances For

source
instance RatFunc.instAdd {K : Type u} [CommRing K] :
Add (RatFunc K)
Equations

- RatFunc.instAdd = { add := RatFunc.add }

source
theorem RatFunc.ofFractionRing_add {K : Type u} [CommRing K] (p q : FractionRing (Polynomial K)) :
{ toFractionRing := p + q } = { toFractionRing := p } + { toFractionRing := q }
source
theorem RatFunc.sub_def {K : Type u_1} [CommRing K] (x✝ x✝¹ : RatFunc K) :
x✝.sub x✝¹ = match x✝, x✝¹ with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p - q }
source
@[irreducible]
def RatFunc.sub {K : Type u_1} [CommRing K] :
RatFunc K → RatFunc K → RatFunc K

Subtraction of rational functions.

Equations

- x✝¹.sub x✝ = match x✝¹, x✝ with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p - q }

Instances For

source
instance RatFunc.instSub {K : Type u} [CommRing K] :
Sub (RatFunc K)
Equations

- RatFunc.instSub = { sub := RatFunc.sub }

source
theorem RatFunc.ofFractionRing_sub {K : Type u} [CommRing K] (p q : FractionRing (Polynomial K)) :
{ toFractionRing := p - q } = { toFractionRing := p } - { toFractionRing := q }
source
@[irreducible]
def RatFunc.neg {K : Type u_1} [CommRing K] :
RatFunc K → RatFunc K

Additive inverse of a rational function.

Equations

- x✝.neg = match x✝ with | { toFractionRing := p } => { toFractionRing := -p }

Instances For

source
theorem RatFunc.neg_def {K : Type u_1} [CommRing K] (x✝ : RatFunc K) :
x✝.neg = match x✝ with | { toFractionRing := p } => { toFractionRing := -p }
source
instance RatFunc.instNeg {K : Type u} [CommRing K] :
Neg (RatFunc K)
Equations

- RatFunc.instNeg = { neg := RatFunc.neg }

source
theorem RatFunc.ofFractionRing_neg {K : Type u} [CommRing K] (p : FractionRing (Polynomial K)) :
{ toFractionRing := -p } = -{ toFractionRing := p }
source
@[irreducible]
def RatFunc.one {K : Type u_1} [CommRing K] :
RatFunc K

The multiplicative unit of rational functions.

Equations

- RatFunc.one = { toFractionRing := 1 }

Instances For

source
theorem RatFunc.one_def {K : Type u_1} [CommRing K] :
RatFunc.one = { toFractionRing := 1 }
source
instance RatFunc.instOne {K : Type u} [CommRing K] :
One (RatFunc K)
Equations

- RatFunc.instOne = { one := RatFunc.one }

source
theorem RatFunc.ofFractionRing_one {K : Type u} [CommRing K] :
{ toFractionRing := 1 } = 1
source
theorem RatFunc.mul_def {K : Type u_1} [CommRing K] (x✝ x✝¹ : RatFunc K) :
x✝.mul x✝¹ = match x✝, x✝¹ with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p * q }
source
@[irreducible]
def RatFunc.mul {K : Type u_1} [CommRing K] :
RatFunc K → RatFunc K → RatFunc K

Multiplication of rational functions.

Equations

- x✝¹.mul x✝ = match x✝¹, x✝ with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p * q }

Instances For

source
instance RatFunc.instMul {K : Type u} [CommRing K] :
Mul (RatFunc K)
Equations

- RatFunc.instMul = { mul := RatFunc.mul }

source
theorem RatFunc.ofFractionRing_mul {K : Type u} [CommRing K] (p q : FractionRing (Polynomial K)) :
{ toFractionRing := p * q } = { toFractionRing := p } * { toFractionRing := q }
source
theorem RatFunc.div_def {K : Type u_1} [CommRing K] [IsDomain K] (x✝ x✝¹ : RatFunc K) :
x✝.div x✝¹ = match x✝, x✝¹ with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p / q }
source
@[irreducible]
def RatFunc.div {K : Type u_1} [CommRing K] [IsDomain K] :
RatFunc K → RatFunc K → RatFunc K

Division of rational functions.

Equations

- x✝¹.div x✝ = match x✝¹, x✝ with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p / q }

Instances For

source
instance RatFunc.instDiv {K : Type u} [CommRing K] [IsDomain K] :
Div (RatFunc K)
Equations

- RatFunc.instDiv = { div := RatFunc.div }

source
theorem RatFunc.ofFractionRing_div {K : Type u} [CommRing K] [IsDomain K] (p q : FractionRing (Polynomial K)) :
{ toFractionRing := p / q } = { toFractionRing := p } / { toFractionRing := q }
source
theorem RatFunc.inv_def {K : Type u_1} [CommRing K] [IsDomain K] (x✝ : RatFunc K) :
x✝.inv = match x✝ with | { toFractionRing := p } => { toFractionRing := p⁻¹ }
source
@[irreducible]
def RatFunc.inv {K : Type u_1} [CommRing K] [IsDomain K] :
RatFunc K → RatFunc K

Multiplicative inverse of a rational function.

Equations

- x✝.inv = match x✝ with | { toFractionRing := p } => { toFractionRing := p⁻¹ }

Instances For

source
instance RatFunc.instInv {K : Type u} [CommRing K] [IsDomain K] :
Inv (RatFunc K)
Equations

- RatFunc.instInv = { inv := RatFunc.inv }

source
theorem RatFunc.ofFractionRing_inv {K : Type u} [CommRing K] [IsDomain K] (p : FractionRing (Polynomial K)) :
{ toFractionRing := p⁻¹ } = { toFractionRing := p }⁻¹
source
theorem RatFunc.mul_inv_cancel {K : Type u} [CommRing K] [IsDomain K] {p : RatFunc K} :
p ≠ 0 → p * p⁻¹ = 1
source
theorem RatFunc.smul_def {K : Type u_2} [CommRing K] {R : Type u_3} [SMul R (FractionRing (Polynomial K))] (x✝ : R) (x✝¹ : RatFunc K) :
RatFunc.smul x✝ x✝¹ = match x✝, x✝¹ with | r, { toFractionRing := p } => { toFractionRing := r • p }
source
@[irreducible]
def RatFunc.smul {K : Type u_2} [CommRing K] {R : Type u_3} [SMul R (FractionRing (Polynomial K))] :
R → RatFunc K → RatFunc K

Scalar multiplication of rational functions.

Equations

- RatFunc.smul x✝¹ x✝ = match x✝¹, x✝ with | r, { toFractionRing := p } => { toFractionRing := r • p }

Instances For

source
instance RatFunc.instSMulOfFractionRingPolynomial {K : Type u} [CommRing K] {R : Type u_1} [SMul R (FractionRing (Polynomial K))] :
SMul R (RatFunc K)
Equations

- RatFunc.instSMulOfFractionRingPolynomial = { smul := RatFunc.smul }

source
theorem RatFunc.ofFractionRing_smul {K : Type u} [CommRing K] {R : Type u_1} [SMul R (FractionRing (Polynomial K))] (c : R) (p : FractionRing (Polynomial K)) :
{ toFractionRing := c • p } = c • { toFractionRing := p }
source
theorem RatFunc.toFractionRing_smul {K : Type u} [CommRing K] {R : Type u_1} [SMul R (FractionRing (Polynomial K))] (c : R) (p : RatFunc K) :
(c • p).toFractionRing = c • p.toFractionRing
source
theorem RatFunc.smul_eq_C_smul {K : Type u} [CommRing K] (x : RatFunc K) (r : K) :
r • x = Polynomial.C r • x
source
theorem RatFunc.mk_smul {K : Type u} [CommRing K] {R : Type u_1} [IsDomain K] [Monoid R] [DistribMulAction R (Polynomial K)] [IsScalarTower R (Polynomial K) (Polynomial K)] (c : R) (p q : Polynomial K) :
RatFunc.mk (c • p) q = c • RatFunc.mk p q
source
instance RatFunc.instIsScalarTowerPolynomial {K : Type u} [CommRing K] {R : Type u_1} [IsDomain K] [Monoid R] [DistribMulAction R (Polynomial K)] [IsScalarTower R (Polynomial K) (Polynomial K)] :
IsScalarTower R (Polynomial K) (RatFunc K)
source
instance RatFunc.instSubsingleton (K : Type u) [CommRing K] [Subsingleton K] :
Subsingleton (RatFunc K)
source
instance RatFunc.instInhabited (K : Type u) [CommRing K] :
Inhabited (RatFunc K)
Equations

- RatFunc.instInhabited K = { default := 0 }

source
instance RatFunc.instNontrivial (K : Type u) [CommRing K] [Nontrivial K] :
Nontrivial (RatFunc K)
source
def RatFunc.toFractionRingRingEquiv (K : Type u) [CommRing K] :
RatFunc K ≃+* FractionRing (Polynomial K)

`RatFunc K` is isomorphic to the field of fractions of `K[X]`, as rings.

This is an auxiliary definition; `simp`-normal form is `IsLocalization.algEquiv`.

Equations

- RatFunc.toFractionRingRingEquiv K = { toFun := RatFunc.toFractionRing, invFun := RatFunc.ofFractionRing, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem RatFunc.toFractionRingRingEquiv_apply (K : Type u) [CommRing K] (self : RatFunc K) :
(toFractionRingRingEquiv K) self = self.toFractionRing
source
def RatFunc.tacticFrac_tac :
Lean.ParserDescr

Solve equations for `RatFunc K` by working in `FractionRing K[X]`.

Equations

- RatFunc.tacticFrac_tac = Lean.ParserDescr.node `RatFunc.tacticFrac_tac 1024 (Lean.ParserDescr.nonReservedSymbol "frac_tac" false)

Instances For

source
def RatFunc.tacticSmul_tac :
Lean.ParserDescr

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

Equations

- RatFunc.tacticSmul_tac = Lean.ParserDescr.node `RatFunc.tacticSmul_tac 1024 (Lean.ParserDescr.nonReservedSymbol "smul_tac" false)

Instances For

source
def RatFunc.instCommMonoid (K : Type u) [CommRing K] :
CommMonoid (RatFunc K)

`RatFunc K` is a commutative monoid.

This is an intermediate step on the way to the full instance `RatFunc.instCommRing`.

Equations

- RatFunc.instCommMonoid K = { toMul := RatFunc.instMul, mul_assoc := ⋯, toOne := RatFunc.instOne, one_mul := ⋯, mul_one := ⋯, npow := npowRec, npow_zero := ⋯, npow_succ := ⋯, mul_comm := ⋯ }

Instances For

source
def RatFunc.instAddCommGroup (K : Type u) [CommRing K] :
AddCommGroup (RatFunc K)

`RatFunc K` is an additive commutative group.

This is an intermediate step on the way to the full instance `RatFunc.instCommRing`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance RatFunc.instCommRing (K : Type u) [CommRing K] :
CommRing (RatFunc K)
Equations

- One or more equations did not get rendered due to their size.

source
def RatFunc.map {R : Type u_3} {S : Type u_4} {F : Type u_5} [CommRing R] [CommRing S] [FunLike F (Polynomial R) (Polynomial S)] [MonoidHomClass F (Polynomial R) (Polynomial S)] (φ : F) (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial S))) :
RatFunc R →* RatFunc 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

- One or more equations did not get rendered due to their size.

Instances For

source
theorem RatFunc.map_apply_ofFractionRing_mk {R : Type u_3} {S : Type u_4} {F : Type u_5} [CommRing R] [CommRing S] [FunLike F (Polynomial R) (Polynomial S)] [MonoidHomClass F (Polynomial R) (Polynomial S)] (φ : F) (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial S))) (n : Polynomial R) (d : ↥(nonZeroDivisors (Polynomial R))) :
(map φ hφ) { toFractionRing := Localization.mk n d } = { toFractionRing := Localization.mk (φ n) ⟨φ ↑d, ⋯⟩ }
source
theorem RatFunc.map_injective {R : Type u_3} {S : Type u_4} {F : Type u_5} [CommRing R] [CommRing S] [FunLike F (Polynomial R) (Polynomial S)] [MonoidHomClass F (Polynomial R) (Polynomial S)] (φ : F) (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial S))) (hf : Function.Injective ⇑φ) :
Function.Injective ⇑(map φ hφ)
source
def RatFunc.mapRingHom {R : Type u_3} {S : Type u_4} {F : Type u_5} [CommRing R] [CommRing S] [FunLike F (Polynomial R) (Polynomial S)] [RingHomClass F (Polynomial R) (Polynomial S)] (φ : F) (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial S))) :
RatFunc R →+* RatFunc 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

- RatFunc.mapRingHom φ hφ = { toMonoidHom := RatFunc.map φ hφ, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
theorem RatFunc.coe_mapRingHom_eq_coe_map {R : Type u_3} {S : Type u_4} {F : Type u_5} [CommRing R] [CommRing S] [FunLike F (Polynomial R) (Polynomial S)] [RingHomClass F (Polynomial R) (Polynomial S)] (φ : F) (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial S))) :
⇑(mapRingHom φ hφ) = ⇑(map φ hφ)
source
def RatFunc.liftMonoidWithZeroHom {G₀ : Type u_1} {R : Type u_3} [CommGroupWithZero G₀] [CommRing R] (φ : Polynomial R →*₀ G₀) (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors G₀)) :
RatFunc R →*₀ 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

- RatFunc.liftMonoidWithZeroHom φ hφ = { toFun := fun (f : RatFunc R) => f.liftOn (fun (p q : Polynomial R) => φ p / φ q) ⋯, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
theorem RatFunc.liftMonoidWithZeroHom_apply_ofFractionRing_mk {G₀ : Type u_1} {R : Type u_3} [CommGroupWithZero G₀] [CommRing R] (φ : Polynomial R →*₀ G₀) (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors G₀)) (n : Polynomial R) (d : ↥(nonZeroDivisors (Polynomial R))) :
(liftMonoidWithZeroHom φ hφ) { toFractionRing := Localization.mk n d } = φ n / φ ↑d
source
theorem RatFunc.liftMonoidWithZeroHom_injective {G₀ : Type u_1} {R : Type u_3} [CommGroupWithZero G₀] [CommRing R] [Nontrivial R] (φ : Polynomial R →*₀ G₀) (hφ : Function.Injective ⇑φ) (hφ' : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors G₀) := ⋯) :
Function.Injective ⇑(liftMonoidWithZeroHom φ hφ')
source
def RatFunc.liftRingHom {L : Type u_2} {R : Type u_3} [Field L] [CommRing R] (φ : Polynomial R →+* L) (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors L)) :
RatFunc R →+* 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

- RatFunc.liftRingHom φ hφ = { toFun := (↑(RatFunc.liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
theorem RatFunc.liftRingHom_apply_ofFractionRing_mk {L : Type u_2} {R : Type u_3} [Field L] [CommRing R] (φ : Polynomial R →+* L) (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors L)) (n : Polynomial R) (d : ↥(nonZeroDivisors (Polynomial R))) :
(liftRingHom φ hφ) { toFractionRing := Localization.mk n d } = φ n / φ ↑d
source
theorem RatFunc.liftRingHom_injective {L : Type u_2} {R : Type u_3} [Field L] [CommRing R] [Nontrivial R] (φ : Polynomial R →+* L) (hφ : Function.Injective ⇑φ) (hφ' : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors L) := ⋯) :
Function.Injective ⇑(liftRingHom φ hφ')
source
instance RatFunc.instField (K : Type u) [CommRing K] [IsDomain K] :
Field (RatFunc K)

Stacks Tag 09FK

Equations

- One or more equations did not get rendered due to their size.

### `RatFunc` as field of fractions of `Polynomial` #

source
instance RatFunc.instAlgebraOfPolynomial (K : Type u) [CommRing K] [IsDomain K] (R : Type u_1) [CommSemiring R] [Algebra R (Polynomial K)] :
Algebra R (RatFunc K)
Equations

- One or more equations did not get rendered due to their size.

source
def RatFunc.coePolynomial {K : Type u} [CommRing K] [IsDomain K] (P : Polynomial K) :
RatFunc K

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

Equations

- ↑P = (algebraMap (Polynomial K) (RatFunc K)) P

Instances For

source
instance RatFunc.instCoePolynomial {K : Type u} [CommRing K] [IsDomain K] :
Coe (Polynomial K) (RatFunc K)
Equations

- RatFunc.instCoePolynomial = { coe := RatFunc.coePolynomial }

source
theorem RatFunc.mk_one {K : Type u} [CommRing K] [IsDomain K] (x : Polynomial K) :
RatFunc.mk x 1 = (algebraMap (Polynomial K) (RatFunc K)) x
source
theorem RatFunc.ofFractionRing_algebraMap {K : Type u} [CommRing K] [IsDomain K] (x : Polynomial K) :
{ toFractionRing := (algebraMap (Polynomial K) (FractionRing (Polynomial K))) x } = (algebraMap (Polynomial K) (RatFunc K)) x
source
def RatFunc.toFractionRingAlgEquiv (K : Type u) [CommRing K] [IsDomain K] (R : Type u_1) [CommSemiring R] [Algebra R (Polynomial K)] :
RatFunc K ≃ₐ[R] FractionRing (Polynomial K)

The equivalence between `RatFunc K` and the field of fractions of `K[X]`

Equations

- RatFunc.toFractionRingAlgEquiv K R = { toEquiv := (RatFunc.toFractionRingRingEquiv K).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

Instances For

source
@[simp]
theorem RatFunc.toFractionRingAlgEquiv_apply (K : Type u) [CommRing K] [IsDomain K] (R : Type u_1) [CommSemiring R] [Algebra R (Polynomial K)] (self : RatFunc K) :
(toFractionRingAlgEquiv K R) self = self.toFractionRing
source
@[simp]
theorem RatFunc.mk_eq_div {K : Type u} [CommRing K] [IsDomain K] (p q : Polynomial K) :
RatFunc.mk p q = (algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q
source
@[simp]
theorem RatFunc.div_smul {K : Type u} [CommRing K] [IsDomain K] {R : Type u_1} [Monoid R] [DistribMulAction R (Polynomial K)] [IsScalarTower R (Polynomial K) (Polynomial K)] (c : R) (p q : Polynomial K) :
(algebraMap (Polynomial K) (RatFunc K)) (c • p) / (algebraMap (Polynomial K) (RatFunc K)) q = c • ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q)
source
theorem RatFunc.algebraMap_apply {K : Type u} [CommRing K] [IsDomain K] {R : Type u_1} [CommSemiring R] [Algebra R (Polynomial K)] (x : R) :
(algebraMap R (RatFunc K)) x = (algebraMap (Polynomial K) (RatFunc K)) ((algebraMap R (Polynomial K)) x) / (algebraMap (Polynomial K) (RatFunc K)) 1
source
theorem RatFunc.map_apply_div_ne_zero {K : Type u} [CommRing K] [IsDomain K] {R : Type u_1} {F : Type u_2} [CommRing R] [IsDomain R] [FunLike F (Polynomial K) (Polynomial R)] [MonoidHomClass F (Polynomial K) (Polynomial R)] (φ : F) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial R))) (p q : Polynomial K) (hq : q ≠ 0) :
(map φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) = (algebraMap (Polynomial R) (RatFunc R)) (φ p) / (algebraMap (Polynomial R) (RatFunc R)) (φ q)
source
@[simp]
theorem RatFunc.map_apply_div {K : Type u} [CommRing K] [IsDomain K] {R : Type u_1} {F : Type u_2} [CommRing R] [IsDomain R] [FunLike F (Polynomial K) (Polynomial R)] [MonoidWithZeroHomClass F (Polynomial K) (Polynomial R)] (φ : F) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial R))) (p q : Polynomial K) :
(map φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) = (algebraMap (Polynomial R) (RatFunc R)) (φ p) / (algebraMap (Polynomial R) (RatFunc R)) (φ q)
source
theorem RatFunc.liftMonoidWithZeroHom_apply_div {K : Type u} [CommRing K] [IsDomain K] {L : Type u_1} [CommGroupWithZero L] (φ : Polynomial K →*₀ L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (p q : Polynomial K) :
(liftMonoidWithZeroHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) = φ p / φ q
source
@[simp]
theorem RatFunc.liftMonoidWithZeroHom_apply_div' {K : Type u} [CommRing K] [IsDomain K] {L : Type u_1} [CommGroupWithZero L] (φ : Polynomial K →*₀ L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (p q : Polynomial K) :
(liftMonoidWithZeroHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p) / (liftMonoidWithZeroHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) q) = φ p / φ q
source
theorem RatFunc.liftRingHom_apply_div {K : Type u} [CommRing K] [IsDomain K] {L : Type u_1} [Field L] (φ : Polynomial K →+* L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (p q : Polynomial K) :
(liftRingHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) = φ p / φ q
source
@[simp]
theorem RatFunc.liftRingHom_apply_div' {K : Type u} [CommRing K] [IsDomain K] {L : Type u_1} [Field L] (φ : Polynomial K →+* L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (p q : Polynomial K) :
(liftRingHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p) / (liftRingHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) q) = φ p / φ q
source
theorem RatFunc.ofFractionRing_comp_algebraMap (K : Type u) [CommRing K] [IsDomain K] :
ofFractionRing ∘ ⇑(algebraMap (Polynomial K) (FractionRing (Polynomial K))) = ⇑(algebraMap (Polynomial K) (RatFunc K))
source
theorem RatFunc.algebraMap_injective (K : Type u) [CommRing K] [IsDomain K] :
Function.Injective ⇑(algebraMap (Polynomial K) (RatFunc K))
source
def RatFunc.mapAlgHom {K : Type u} [CommRing K] [IsDomain K] {R : Type u_2} {S : Type u_3} [CommRing R] [IsDomain R] [CommSemiring S] [Algebra S (Polynomial K)] [Algebra S (Polynomial R)] (φ : Polynomial K →ₐ[S] Polynomial R) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial R))) :
RatFunc K →ₐ[S] RatFunc R

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

- RatFunc.mapAlgHom φ hφ = { toRingHom := RatFunc.mapRingHom φ hφ, commutes' := ⋯ }

Instances For

source
theorem RatFunc.coe_mapAlgHom_eq_coe_map {K : Type u} [CommRing K] [IsDomain K] {R : Type u_2} {S : Type u_3} [CommRing R] [IsDomain R] [CommSemiring S] [Algebra S (Polynomial K)] [Algebra S (Polynomial R)] (φ : Polynomial K →ₐ[S] Polynomial R) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial R))) :
⇑(mapAlgHom φ hφ) = ⇑(map φ hφ)
source
def RatFunc.liftAlgHom {K : Type u} [CommRing K] [IsDomain K] {L : Type u_1} {S : Type u_3} [Field L] [CommSemiring S] [Algebra S (Polynomial K)] [Algebra S L] (φ : Polynomial K →ₐ[S] L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) :
RatFunc K →ₐ[S] 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

- RatFunc.liftAlgHom φ hφ = { toRingHom := RatFunc.liftRingHom φ.toRingHom hφ, commutes' := ⋯ }

Instances For

source
theorem RatFunc.liftAlgHom_apply_ofFractionRing_mk {K : Type u} [CommRing K] [IsDomain K] {L : Type u_1} {S : Type u_3} [Field L] [CommSemiring S] [Algebra S (Polynomial K)] [Algebra S L] (φ : Polynomial K →ₐ[S] L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (n : Polynomial K) (d : ↥(nonZeroDivisors (Polynomial K))) :
(liftAlgHom φ hφ) { toFractionRing := Localization.mk n d } = φ n / φ ↑d
source
theorem RatFunc.liftAlgHom_injective {K : Type u} [CommRing K] [IsDomain K] {L : Type u_1} {S : Type u_3} [Field L] [CommSemiring S] [Algebra S (Polynomial K)] [Algebra S L] (φ : Polynomial K →ₐ[S] L) (hφ : Function.Injective ⇑φ) (hφ' : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L) := ⋯) :
Function.Injective ⇑(liftAlgHom φ hφ')
source
@[simp]
theorem RatFunc.liftAlgHom_apply_div' {K : Type u} [CommRing K] [IsDomain K] {L : Type u_1} {S : Type u_3} [Field L] [CommSemiring S] [Algebra S (Polynomial K)] [Algebra S L] (φ : Polynomial K →ₐ[S] L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (p q : Polynomial K) :
(liftAlgHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p) / (liftAlgHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) q) = φ p / φ q
source
theorem RatFunc.liftAlgHom_apply_div {K : Type u} [CommRing K] [IsDomain K] {L : Type u_1} {S : Type u_3} [Field L] [CommSemiring S] [Algebra S (Polynomial K)] [Algebra S L] (φ : Polynomial K →ₐ[S] L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (p q : Polynomial K) :
(liftAlgHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) = φ p / φ q
source
instance RatFunc.instIsFractionRingPolynomial (K : Type u) [CommRing K] [IsDomain K] :
IsFractionRing (Polynomial K) (RatFunc K)

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

source
theorem RatFunc.algebraMap_ne_zero {K : Type u} [CommRing K] [IsDomain K] {x : Polynomial K} (hx : x ≠ 0) :
(algebraMap (Polynomial K) (RatFunc K)) x ≠ 0
source
@[simp]
theorem RatFunc.liftOn_div {K : Type u} [CommRing K] [IsDomain 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 ∈ nonZeroDivisors (Polynomial K) → q' ∈ nonZeroDivisors (Polynomial K) → q' * p = q * p' → f p q = f p' q' := ⋯) :
((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q).liftOn f H = f p q
source
@[simp]
theorem RatFunc.liftOn'_div {K : Type u} [CommRing K] [IsDomain 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) :
((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q).liftOn' f H = f p q
source
theorem RatFunc.induction_on {K : Type u} [CommRing K] [IsDomain K] {P : RatFunc K → Prop} (x : RatFunc K) (f : ∀ (p q : Polynomial K), q ≠ 0 → P ((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`.

source
theorem RatFunc.ofFractionRing_mk' {K : Type u} [CommRing K] [IsDomain K] (x : Polynomial K) (y : ↥(nonZeroDivisors (Polynomial K))) :
{ toFractionRing := IsLocalization.mk' (FractionRing (Polynomial K)) x y } = IsLocalization.mk' (RatFunc K) x y
source
theorem RatFunc.mk_eq_mk' {K : Type u} [CommRing K] [IsDomain K] (f : Polynomial K) {g : Polynomial K} (hg : g ≠ 0) :
RatFunc.mk f g = IsLocalization.mk' (RatFunc K) f ⟨g, ⋯⟩
source
@[simp]
theorem RatFunc.ofFractionRing_eq {K : Type u} [CommRing K] [IsDomain K] :
ofFractionRing = ⇑(IsLocalization.algEquiv (nonZeroDivisors (Polynomial K)) (FractionRing (Polynomial K)) (RatFunc K))
source
@[simp]
theorem RatFunc.toFractionRing_eq {K : Type u} [CommRing K] [IsDomain K] :
toFractionRing = ⇑(IsLocalization.algEquiv (nonZeroDivisors (Polynomial K)) (RatFunc K) (FractionRing (Polynomial K)))
source
@[simp]
theorem RatFunc.toFractionRingRingEquiv_symm_eq {K : Type u} [CommRing K] [IsDomain K] :
(toFractionRingRingEquiv K).symm = (IsLocalization.algEquiv (nonZeroDivisors (Polynomial K)) (FractionRing (Polynomial K)) (RatFunc K)).toRingEquiv
source
def RatFunc.liftAlgebra (R : Type u_1) (L : Type u_2) [CommRing R] [Field L] [IsDomain R] [Algebra (Polynomial R) L] [FaithfulSMul (Polynomial R) L] :
Algebra (RatFunc R) L

`FractionRing.liftAlgebra` specialized to `RatFunc R`.

This is a scoped instance because it creates a diamond when `L = RatFunc R`.

Equations

- RatFunc.liftAlgebra R L = (IsFractionRing.lift ⋯).toAlgebra

Instances For

source
instance RatFunc.isScalarTower_liftAlgebra (R : Type u_1) (L : Type u_2) [CommRing R] [Field L] [IsDomain R] [Algebra (Polynomial R) L] [FaithfulSMul (Polynomial R) L] :
IsScalarTower (Polynomial R) (RatFunc R) L

`FractionRing.isScalarTower_liftAlgebra` specialized to `RatFunc R`.

source
instance RatFunc.faithfulSMul (K : Type u_3) (E : Type u_4) [Field K] [Field E] [Algebra K E] [FaithfulSMul K E] :
FaithfulSMul (Polynomial K) (RatFunc E)

`FractionRing.instFaithfulSMul` specialized to `RatFunc R`.

source
theorem RatFunc.rank_ratFunc_ratFunc (k : Type u_3) (K : Type u_4) [Field k] [Field K] [Algebra k K] [Algebra.IsAlgebraic k K] :
Module.rank (RatFunc k) (RatFunc K) = Module.rank k K
source
theorem RatFunc.finrank_ratFunc_ratFunc (k : Type u_3) (K : Type u_4) [Field k] [Field K] [Algebra k K] [Algebra.IsAlgebraic k K] :
Module.finrank (RatFunc k) (RatFunc K) = Module.finrank k K
source
instance RatFunc.instIsScalarTowerOfIsDomainOfPolynomial (R₀ : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring R₀] [CommSemiring R] [CommRing A] [IsDomain A] [Algebra R₀ (Polynomial A)] [SMul R₀ R] [Algebra R (Polynomial A)] [IsScalarTower R₀ R (Polynomial A)] :
IsScalarTower R₀ R (RatFunc A)

Let `RatFunc A / A[X] / R / R₀` be a tower. If `A[X] / R / R₀` is a scalar tower then so is `RatFunc A / R / R₀`.

source
instance RatFunc.instIsScalarTowerOfPolynomial (R : Type u_1) (A : Type u_2) (K : Type u_3) [CommRing A] [IsDomain A] [Field K] [Algebra (Polynomial A) K] [FaithfulSMul (Polynomial A) K] [CommSemiring R] [Algebra R (Polynomial A)] [SMul R K] [IsScalarTower R (Polynomial A) K] :
IsScalarTower R (RatFunc A) K

Let `K / RatFunc A / A[X] / R` be a tower. If `K / A[X] / R` is a scalar tower then so is `K / RatFunc A / R`.

source
instance RatFunc.instIsScalarTowerOfPolynomial_1 (A : Type u_1) (k : Type u_2) (K : Type u_3) [CommRing A] [IsDomain A] [Field k] [Field K] [Algebra (Polynomial A) k] [Algebra (Polynomial A) K] [SMul k K] [FaithfulSMul (Polynomial A) k] [FaithfulSMul (Polynomial A) K] [IsScalarTower (Polynomial A) k K] :
IsScalarTower (RatFunc A) k K

Let `K / k / RatFunc A / A[X]` be a tower. If `K / k / A[X]` is a scalar tower then so is `K / k / RatFunc A`.

### Numerator and denominator #

source
def RatFunc.numDenom {K : Type u} [Field K] (x : RatFunc K) :
Polynomial K × Polynomial K

`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

source
@[simp]
theorem RatFunc.numDenom_div {K : Type u} [Field K] (p : Polynomial K) {q : Polynomial K} (hq : q ≠ 0) :
((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q).numDenom = (Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q), Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q))
source
def RatFunc.num {K : Type u} [Field K] (x : RatFunc K) :
Polynomial K

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

Equations

- x.num = x.numDenom.1

Instances For

source
@[simp]
theorem RatFunc.num_zero {K : Type u} [Field K] :
num 0 = 0
source
@[simp]
theorem RatFunc.num_div {K : Type u} [Field K] (p q : Polynomial K) :
((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q).num = Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)
source
@[simp]
theorem RatFunc.num_one {K : Type u} [Field K] :
num 1 = 1
source
@[simp]
theorem RatFunc.num_algebraMap {K : Type u} [Field K] (p : Polynomial K) :
((algebraMap (Polynomial K) (RatFunc K)) p).num = p
source
theorem RatFunc.num_div_dvd {K : Type u} [Field K] (p : Polynomial K) {q : Polynomial K} (hq : q ≠ 0) :
((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q).num ∣ p
source
@[simp]
theorem RatFunc.num_div_dvd' {K : Type u} [Field K] (p : Polynomial K) {q : Polynomial K} (hq : q ≠ 0) :
Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q) ∣ p

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

source
def RatFunc.denom {K : Type u} [Field K] (x : RatFunc K) :
Polynomial K

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

Equations

- x.denom = x.numDenom.2

Instances For

source
@[simp]
theorem RatFunc.denom_div {K : Type u} [Field K] (p : Polynomial K) {q : Polynomial K} (hq : q ≠ 0) :
((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q).denom = Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q)
source
theorem RatFunc.monic_denom {K : Type u} [Field K] (x : RatFunc K) :
x.denom.Monic
source
theorem RatFunc.denom_ne_zero {K : Type u} [Field K] (x : RatFunc K) :
x.denom ≠ 0
source
@[simp]
theorem RatFunc.denom_zero {K : Type u} [Field K] :
denom 0 = 1
source
@[simp]
theorem RatFunc.denom_one {K : Type u} [Field K] :
denom 1 = 1
source
@[simp]
theorem RatFunc.denom_algebraMap {K : Type u} [Field K] (p : Polynomial K) :
((algebraMap (Polynomial K) (RatFunc K)) p).denom = 1
source
@[simp]
theorem RatFunc.denom_div_dvd {K : Type u} [Field K] (p q : Polynomial K) :
((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q).denom ∣ q
source
@[simp]
theorem RatFunc.num_div_denom {K : Type u} [Field K] (x : RatFunc K) :
(algebraMap (Polynomial K) (RatFunc K)) x.num / (algebraMap (Polynomial K) (RatFunc K)) x.denom = x
source
theorem RatFunc.isCoprime_num_denom {K : Type u} [Field K] (x : RatFunc K) :
IsCoprime x.num x.denom
source
@[simp]
theorem RatFunc.num_eq_zero_iff {K : Type u} [Field K] {x : RatFunc K} :
x.num = 0 ↔ x = 0
source
theorem RatFunc.num_ne_zero {K : Type u} [Field K] {x : RatFunc K} (hx : x ≠ 0) :
x.num ≠ 0
source
theorem RatFunc.num_mul_eq_mul_denom_iff {K : Type u} [Field K] {x : RatFunc K} {p q : Polynomial K} (hq : q ≠ 0) :
x.num * q = p * x.denom ↔ x = (algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q
source
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
source
theorem RatFunc.num_denom_neg {K : Type u} [Field K] (x : RatFunc K) :
(-x).num * x.denom = -x.num * (-x).denom
source
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
source
theorem RatFunc.num_dvd {K : Type u} [Field K] {x : RatFunc K} {p : Polynomial K} (hp : p ≠ 0) :
x.num ∣ p ↔ ∃ (q : Polynomial K), q ≠ 0 ∧ x = (algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q
source
theorem RatFunc.denom_dvd {K : Type u} [Field K] {x : RatFunc K} {q : Polynomial K} (hq : q ≠ 0) :
x.denom ∣ q ↔ ∃ (p : Polynomial K), x = (algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q
source
theorem RatFunc.num_mul_dvd {K : Type u} [Field K] (x y : RatFunc K) :
(x * y).num ∣ x.num * y.num
source
theorem RatFunc.denom_mul_dvd {K : Type u} [Field K] (x y : RatFunc K) :
(x * y).denom ∣ x.denom * y.denom
source
theorem RatFunc.denom_add_dvd {K : Type u} [Field K] (x y : RatFunc K) :
(x + y).denom ∣ x.denom * y.denom
source
theorem RatFunc.map_denom_ne_zero {K : Type u} [Field K] {L : Type u_1} {F : Type u_2} [Zero L] [FunLike F (Polynomial K) L] [ZeroHomClass F (Polynomial K) L] (φ : F) (hφ : Function.Injective ⇑φ) (f : RatFunc K) :
φ f.denom ≠ 0
source
theorem RatFunc.map_apply {K : Type u} [Field K] {R : Type u_1} {F : Type u_2} [CommRing R] [IsDomain R] [FunLike F (Polynomial K) (Polynomial R)] [MonoidHomClass F (Polynomial K) (Polynomial R)] (φ : F) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial R))) (f : RatFunc K) :
(map φ hφ) f = (algebraMap (Polynomial R) (RatFunc R)) (φ f.num) / (algebraMap (Polynomial R) (RatFunc R)) (φ f.denom)
source
theorem RatFunc.liftMonoidWithZeroHom_apply {K : Type u} [Field K] {L : Type u_1} [CommGroupWithZero L] (φ : Polynomial K →*₀ L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (f : RatFunc K) :
(liftMonoidWithZeroHom φ hφ) f = φ f.num / φ f.denom
source
theorem RatFunc.liftRingHom_apply {K : Type u} [Field K] {L : Type u_1} [Field L] (φ : Polynomial K →+* L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (f : RatFunc K) :
(liftRingHom φ hφ) f = φ f.num / φ f.denom
source
theorem RatFunc.liftAlgHom_apply {K : Type u} [Field K] {L : Type u_1} {S : Type u_2} [Field L] [CommSemiring S] [Algebra S (Polynomial K)] [Algebra S L] (φ : Polynomial K →ₐ[S] L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (f : RatFunc K) :
(liftAlgHom φ hφ) f = φ f.num / φ f.denom
source
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
source
instance RatFunc.instCharP {K : Type u} [Field K] {p : ℕ} [CharP K p] :
CharP (RatFunc K) p
source
instance RatFunc.instExpChar {K : Type u} [Field K] {p : ℕ} [ExpChar K p] :
ExpChar (RatFunc K) p
source
instance RatFunc.instCharZero {K : Type u} [Field K] [CharZero K] :
CharZero (RatFunc K)