RatFunc.algebraMap_ne_zero
theorem RatFunc.algebraMap_ne_zero :
∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {x : Polynomial K},
x ≠ 0 → (algebraMap (Polynomial K) (RatFunc K)) x ≠ 0
The theorem `RatFunc.algebraMap_ne_zero` states that for any commutative ring `K` which is also an integral domain, and any non-zero polynomial `x` with coefficients in `K`, the algebra map from the ring of polynomials over `K` to the field of rational functions over `K`, applied to `x`, is also not zero. Essentially, this means that non-zero polynomials map to non-zero elements in the field of rational functions when using the algebra map.
More concisely: For any commutative integral domain K and non-zero polynomial x in K[X], the algebra map from K[X] to K(X) maps x to a non-zero rational function.
|
RatFunc.denom_X
theorem RatFunc.denom_X : ∀ {K : Type u} [inst : Field K], RatFunc.X.denom = 1
The theorem `RatFunc.denom_X` states that for any field `K`, the denominator of the rational function represented by the polynomial variable (also known as indeterminate), i.e., `RatFunc.X`, is always 1. In other words, when we treat a polynomial variable as a rational function in any field, its denominator, when normalized so that it's monic, is invariably 1.
More concisely: For any field K, the denominator of the rational function represented by the polynomial variable X in Lean 4 is equal to 1.
|
RatFunc.denom_div
theorem RatFunc.denom_div :
∀ {K : Type u} [inst : Field K] (p : Polynomial K) {q : Polynomial K},
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)
The theorem `RatFunc.denom_div` states that for any field `K` and for any two polynomials `p` and `q` from `K`, where `q` is not zero, the denominator of the rational function resulting from the division of the algebraic mappings of `p` and `q` into `RatFunc K` is equivalent to the product of the inverse of the leading coefficient of the polynomial `q / gcd(p, q)` and the polynomial `q / gcd(p, q)`. In other words, if you convert the polynomials `p` and `q` into rational functions and divide them, the denominator of the result is determined by the leading coefficient and the greatest common divisor of the original polynomials.
More concisely: Given a field `K` and two polynomials `p` and `q` in `K` with `q` not zero, the denominator of the rational function `(alg_map p : RatFunc K) / (alg_map q : RatFunc K)` is equivalent to `(lc_coeff q / gcd p q) * q / gcd p q`.
|
RatFunc.num_algebraMap
theorem RatFunc.num_algebraMap :
∀ {K : Type u} [inst : Field K] (p : Polynomial K), ((algebraMap (Polynomial K) (RatFunc K)) p).num = p
The theorem `RatFunc.num_algebraMap` states that for any field `K` and any polynomial `p` over `K`, the numerator of the rational function obtained by embedding the polynomial `p` into the field `K` of rational functions using the algebraic structure's map, is `p` itself. In other words, this theorem states that under this particular mapping, the polynomial `p` maps to a rational function whose numerator is `p` and the denominator is implicitly 1.
More concisely: The theorem asserts that under the algebraic structure map, a polynomial over a field maps to a rational function with that polynomial as its numerator.
|
RatFunc.num_mul_eq_mul_denom_iff
theorem RatFunc.num_mul_eq_mul_denom_iff :
∀ {K : Type u} [inst : Field K] {x : RatFunc K} {p q : Polynomial K},
q ≠ 0 →
(x.num * q = p * x.denom ↔
x = (algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q)
This theorem states that for any field `K` and any rational function `x` of type `RatFunc K`, along with any two polynomials `p` and `q` in `K` where `q` is not equal to zero, the equality of the product of the numerator of `x` and `q` with the product of `p` and the denominator of `x` is equivalent to `x` being equal to the division of the algebra map applied to `p` by the algebra map applied to `q`. Here, the algebra map is a function that embeds the ring of polynomials into the field of rational functions.
More concisely: For any field `K`, rational function `x : RatFunc K`, polynomials `p`, `q ≠ 0` in `K`, the equality `(numerator x) * q = p * (denominator x)` holds if and only if `x = algebraMap K p / algebraMap K q`.
|
RatFunc.eval_add
theorem RatFunc.eval_add :
∀ {K : Type u} [inst : Field K] {L : Type u_1} [inst_1 : Field L] (f : K →+* L) (a : L) {x y : RatFunc K},
Polynomial.eval₂ f a x.denom ≠ 0 →
Polynomial.eval₂ f a y.denom ≠ 0 → RatFunc.eval f a (x + y) = RatFunc.eval f a x + RatFunc.eval f a y
The theorem `RatFunc.eval_add` states that for any fields `K` and `L`, a ring homomorphism `f` from `K` to `L`, a value `a` in `L`, and any two rational functions `x` and `y` in `K`, the evaluation of the sum of `x` and `y` at `a` is equal to the sum of the evaluations of `x` and `y` at `a`, given that the evaluations of the denominators of `x` and `y` at `a` are not zero. This asserts that the evaluation function is an additive homomorphism except when a denominator evaluates to `0`.
The comment also provides a counterexample where this homomorphism property is not held: `eval _ 1 (X / (X-1)) + eval _ 1 (-1 / (X-1)) = 0`, which is not equal to `1 = eval _ 1 ((X-1) / (X-1))`.
For simpler but less general hypotheses, refer to the theorem `RatFunc.eval₂_denom_ne_zero`.
More concisely: For any ring homomorphism `f` from field `K` to field `L`, and for any rational functions `x` and `y` in `K` with non-zero denominators at `a` in `L`, the evaluation of `x + y` at `a` equals the sum of the evaluations of `x` and `y` at `a` (i.e., `eval a (x + y) = eval a x + eval a y`).
|
RatFunc.liftMonoidWithZeroHom_apply_div
theorem RatFunc.liftMonoidWithZeroHom_apply_div :
∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {L : Type u_1} [inst_2 : CommGroupWithZero L]
(φ : Polynomial K →*₀ L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L))
(p q : Polynomial K),
(RatFunc.liftMonoidWithZeroHom φ hφ)
((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) =
φ p / φ q
This theorem states that for any commutative ring `K` and commutative group with zero `L`, given a multiplication-preserving function `φ` from the polynomials over `K` to `L`, which respects the set of non-zero divisors in both structures, then for any two polynomials `p` and `q` in `K`, the result of mapping the ratio of `p` and `q` under the function `RatFunc.liftMonoidWithZeroHom φ hφ` (which lifts the function φ to the field of fractions) is equal to the ratio of φ applied to `p` and `q` separately. In mathematical terms, it states that given a homomorphism that preserves non-zero divisors, the homomorphism commutes with the forming of ratios in the field of fractions.
More concisely: Given a homomorphism φ from the polynomial ring over a commutative ring to a commutative group that respects non-zero divisors, the ratio of polynomials in the field of fractions is equal to the ratio of their images under φ.
|
RatFunc.denom_zero
theorem RatFunc.denom_zero : ∀ {K : Type u} [inst : Field K], RatFunc.denom 0 = 1
This theorem, `RatFunc.denom_zero`, states that for any type `K`, which is a field, the denominator of the zero rational function (`RatFunc 0`) is equal to `1`. In other words, in any field, the denominator of the rational function representing zero is normalized to be the monic polynomial `1`.
More concisely: In any field, the denominator of the zero rational function is equal to 1.
|
RatFunc.denom_C
theorem RatFunc.denom_C : ∀ {K : Type u} [inst : Field K] (c : K), (RatFunc.C c).denom = 1
This theorem, `RatFunc.denom_C`, states that for any field `K` and any element `c` in this field, the denominator of the constant rational function `RatFunc.C c` (which represents the constant rational function `c`) is `1`. In other words, when a constant is viewed as a rational function, its denominator is always `1`.
More concisely: For any field `K` and constant `c` in `K`, the denominator of the constant rational function `RatFunc.C c` is `1`.
|
RatFunc.mk_one'
theorem RatFunc.mk_one' :
∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (p : Polynomial K),
RatFunc.mk p 1 = { toFractionRing := (algebraMap (Polynomial K) (FractionRing (Polynomial K))) p }
This theorem states that for any commutative ring `K` that is also an integral domain, and any polynomial `p` with coefficients in `K`, creating a rational function from `p` and `1` yields the same result as mapping `p` through an algebra embedding into the fraction ring of `K` polynomials. In simpler terms, it asserts that the rational function `p / 1` is equivalent to the algebraic construction of the polynomial `p` itself in the fraction ring of polynomials over `K`.
More concisely: For any commutative integral domain `K` and polynomial `p` over `K`, the rational function `p / 1` is equivalent to the polynomial `p` in the fraction ring of `K` polynomials.
|
RatFunc.ofFractionRing_smul
theorem RatFunc.ofFractionRing_smul :
∀ {K : Type u} [inst : CommRing K] {R : Type u_1} [inst_1 : SMul R (FractionRing (Polynomial K))] (c : R)
(p : FractionRing (Polynomial K)), { toFractionRing := c • p } = c • { toFractionRing := p }
This theorem, `RatFunc.ofFractionRing_smul`, states that for any commutative ring `K`, any type `R` that allows scalar multiplication with the fraction ring of polynomials over `K`, any scalar `c` of type `R`, and any polynomial `p` in the fraction ring of polynomials over `K`, scalar multiplication of `c` with the structure `{ toFractionRing := p }` is equal to the structure `{ toFractionRing := c • p }`. In simpler terms, it says that scaling a polynomial in the fraction ring is the same as scaling the polynomial first and then taking it to the fraction ring.
More concisely: For any commutative ring K, any type R admitting scalar multiplication with the fraction ring of polynomials over K, and for any scalar c in R and polynomial p in the fraction ring of polynomials over K, the scalar multiplication of c with the polynomial p is equal to the polynomial obtained by scaling p and then taking it to the fraction ring.
|
Mathlib.FieldTheory.RatFunc._auxLemma.4
theorem Mathlib.FieldTheory.RatFunc._auxLemma.4 :
∀ {K : Type u} [inst : CommRing K] (p q : FractionRing (Polynomial K)),
{ toFractionRing := p } * { toFractionRing := q } = { toFractionRing := p * q }
This theorem states that for any commutative ring `K` and any two elements `p` and `q` in the fraction ring of the polynomial ring over `K` (denoted as `FractionRing (Polynomial K)`), the product of `p` and `q` in this fraction ring is the same as if we multiplied `p` and `q` as polynomials first and then put them in the fraction ring. This essentially tells us that the fraction ring operation is compatible with the multiplication operation in the ring.
More concisely: For any commutative ring K, the multiplication in the fraction ring of polynomials over K agrees with the quotient of their multiplication as polynomials.
|
RatFunc.denom_algebraMap
theorem RatFunc.denom_algebraMap :
∀ {K : Type u} [inst : Field K] (p : Polynomial K), ((algebraMap (Polynomial K) (RatFunc K)) p).denom = 1 := by
sorry
This theorem states that for any field `K` and any polynomial `p` over `K`, if we map `p` from the polynomial ring over `K` to the ring of rational functions over `K` using the `algebraMap` function, then the denominator of the resulting rational function, when normalized so that it is monic (leading coefficient is 1), is always 1. In other words, the algebraic mapping of a polynomial into a rational function always results in a rational function with a denominator of 1.
More concisely: For any field `K` and polynomial `p` over `K`, the image of `p` under the algebra map from the polynomial ring to the rational function ring over `K` is a rational function with a monic denominator equal to 1.
|
RatFunc.num_C
theorem RatFunc.num_C : ∀ {K : Type u} [inst : Field K] (c : K), (RatFunc.C c).num = Polynomial.C c
The theorem `RatFunc.num_C` states that for any type `K` that forms a field, and for any element `c` of `K`, the numerator of the constant rational function `c` (denoted as `RatFunc.C c`) is equal to the constant polynomial `c` (denoted as `Polynomial.C c`). In other words, when we consider a constant as a rational function, its numerator is just the same constant considered as a polynomial.
More concisely: For any field `K` and constant `c` in `K`, `RatFunc.C c` equals `Polynomial.C c`.
|
RatFunc.ofFractionRing_zero
theorem RatFunc.ofFractionRing_zero : ∀ {K : Type u} [inst : CommRing K], { toFractionRing := 0 } = 0
This theorem states that for any type `K` that is a commutative ring, the fraction ring of zero is zero. In more mathematical terms, if `K` is a commutative ring, then the rational function mapping to the fraction ring of zero is equal to zero. This is a fundamental property of fraction rings in ring theory.
More concisely: For any commutative ring `K`, the constant map from `K` to its fraction ring mapping all elements to the fraction `0/1` is equal to the zero homomorphism.
|
RatFunc.num_X
theorem RatFunc.num_X : ∀ {K : Type u} [inst : Field K], RatFunc.X.num = Polynomial.X
This theorem states that for any type `K` that forms a field, the numerator of the rational function that corresponds to the polynomial variable (or indeterminate) in the rational functions over `K` is equal to the polynomial variable in the polynomials over `K`. In mathematical terms, if we consider `RatFunc.X` as a rational function which is simply the polynomial variable considered as a rational function, then its numerator, when the denominator is normalized to be monic, is just the polynomial variable itself.
More concisely: For any field `K`, the numerator of the rational function `RatFunc.X` over `K` is equal to the polynomial variable `X` in the polynomials over `K`.
|
RatFunc.eval_mul
theorem RatFunc.eval_mul :
∀ {K : Type u} [inst : Field K] {L : Type u_1} [inst_1 : Field L] (f : K →+* L) (a : L) {x y : RatFunc K},
Polynomial.eval₂ f a x.denom ≠ 0 →
Polynomial.eval₂ f a y.denom ≠ 0 → RatFunc.eval f a (x * y) = RatFunc.eval f a x * RatFunc.eval f a y
The theorem `RatFunc.eval_mul` states that for any two rational functions `x` and `y` in a field `K`, and a ring homomorphism `f` from `K` to another field `L`, the evaluation of the product of `x` and `y` at a point `a` in `L` is equal to the product of the evaluations of `x` and `y` at `a`, provided that the evaluations of the denominators of `x` and `y` at `a` are both non-zero. In other words, the evaluation function `RatFunc.eval` behaves like a multiplicative homomorphism except when the denominator of a rational function evaluates to zero. An example where it does not behave as such is provided: `eval _ 0 X * eval _ 0 (1/X) = 0 ≠ 1 = eval _ 0 1 = eval _ 0 (X * 1/X)`. A related theorem `RatFunc.eval₂_denom_ne_zero` offers a less general but simpler set of hypotheses.
More concisely: For any rational functions $x$ and $y$ in a field $K$, and a ring homomorphism $f$ from $K$ to another field $L$, if the evaluations of the denominators of $x$ and $y$ at a point $a$ in $L$ are both non-zero, then the evaluation of the product of $x$ and $y$ at $a$ equals the product of the evaluations of $x$ and $y$ at $a$.
|
RatFunc.num_div
theorem RatFunc.num_div :
∀ {K : Type u} [inst : 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)
This theorem states that for any field `K` and any two polynomials `p` and `q` over `K`, the numerator of the rational function obtained by dividing the algebraic map of `p` by the algebraic map of `q` is equal to the constant polynomial of the inverse of the leading coefficient of the polynomial obtained by dividing `q` by the greatest common divisor of `p` and `q` multiplied by the polynomial obtained by dividing `p` by the greatest common divisor of `p` and `q`. In other words, this theorem provides a formula to compute the numerator of the rational function corresponding to the fraction of two polynomials in terms of the constant polynomial, the leading coefficient, and the greatest common divisor.
More concisely: For polynomials `p` and `q` over a field `K`, the numerator of `p / q` is `(lc(gcd(p, q)).inv * (p / gcd(p, q)))`, where `lc` denotes the leading coefficient and `inv` the multiplicative inverse.
|
RatFunc.liftMonoidWithZeroHom_apply_ofFractionRing_mk
theorem RatFunc.liftMonoidWithZeroHom_apply_ofFractionRing_mk :
∀ {G₀ : Type u_1} {R : Type u_3} [inst : CommGroupWithZero G₀] [inst_1 : CommRing R] (φ : Polynomial R →*₀ G₀)
(hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors G₀)) (n : Polynomial R)
(d : ↥(nonZeroDivisors (Polynomial R))),
(RatFunc.liftMonoidWithZeroHom φ hφ) { toFractionRing := Localization.mk n d } = φ n / φ ↑d
This theorem states that for any commutative group with zero `G₀` and any commutative ring `R`, if there exists a monoid with zero homomorphism `φ` from the polynomials over `R` to `G₀` such that the set of non-zero divisors in the polynomials over `R` is a subset of the preimage under `φ` of the set of non-zero divisors in `G₀`, then for any polynomial `n` over `R` and any element `d` in the set of non-zero divisors of the polynomials over `R`, the application of the lift of the monoid with zero homomorphism `φ` to the fraction ring element represented by the ordered pair `(n, d)` equals to the ratio of the application of `φ` to `n` and the application of `φ` to `d`. In other words, we can lift the homomorphism `φ` to work with fractions of polynomials, and this lift behaves as expected on elements of the form `(n, d)`.
More concisely: If `φ` is a monoid homomorphism from the polynomials over a commutative ring `R` to a commutative group with zero `G₀`, with the set of non-zero divisors in `R[X]` contained in the preimage of non-zero divisors in `G₀`, then `φ` extends to a homomorphism on the fraction ring of `R[X]`, preserving ratios of non-zero divisors.
|
RatFunc.denom_ne_zero
theorem RatFunc.denom_ne_zero : ∀ {K : Type u} [inst : Field K] (x : RatFunc K), x.denom ≠ 0
The theorem `RatFunc.denom_ne_zero` states that for any rational function `x` over a generic field `K`, the denominator of `x`, when normalized to be monic, is not equal to zero. This means, the monic normalization of the denominator of any rational function in any field never results in the zero polynomial.
More concisely: For any rational function over a field, the normalized denominator is never the zero polynomial.
|
RatFunc.num_zero
theorem RatFunc.num_zero : ∀ {K : Type u} [inst : Field K], RatFunc.num 0 = 0
The theorem `RatFunc.num_zero` states that for any type `K` that is a field, the numerator of the zero rational function (which is represented as `RatFunc.num 0`) is zero. In other words, if you have a rational function which is zero, then its numerator is also zero. This is applicable in any field `K`.
More concisely: For any field `K`, the numerator of the zero rational function is zero.
|
RatFunc.mk_eq_div
theorem RatFunc.mk_eq_div :
∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (p q : Polynomial K),
RatFunc.mk p q = (algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q
This theorem, `RatFunc.mk_eq_div`, states that for any type `K` with a commutative ring structure and domain structure, and for any two polynomials `p` and `q` over `K`, the rational function created by `RatFunc.mk p q` is equal to the division of the algebraic mapping of `p` over the algebraic mapping of `q`. In simpler terms, it states that creating a rational function with `p` and `q` is the same as dividing the algebraic representation of `p` by the algebraic representation of `q`. This theorem relates the construction of rational functions to division in the algebra of rational functions over polynomials.
More concisely: For any commutative ring and domain `K`, `RatFunc.mk (p : polynomial K) (q : polynomial K) = ( Polandsum.algebraMap K p) / (Polandsum.algebraMap K q)` in the algebra of rational functions over polynomials.
|
RatFunc.num_div_denom
theorem RatFunc.num_div_denom :
∀ {K : Type u} [inst : Field K] (x : RatFunc K),
(algebraMap (Polynomial K) (RatFunc K)) x.num / (algebraMap (Polynomial K) (RatFunc K)) x.denom = x
This theorem states that for any field `K` and any rational function `x` over `K`, the rational function obtained by dividing the image of the numerator of `x` under the algebraic embedding from `Polynomial K` to `RatFunc K` by the image of the denominator of `x` under the same embedding, is equal to `x` itself. In other words, representing a rational function as the division of its numerator by its denominator under the algebraic ring homomorphism from polynomials to rational functions preserves the original rational function.
More concisely: The algebraic embedding of polynomials to rational functions preserves the division of numerator by denominator of a rational function.
|
RatFunc.ofFractionRing_injective
theorem RatFunc.ofFractionRing_injective :
∀ {K : Type u} [inst : CommRing K], Function.Injective RatFunc.ofFractionRing
The theorem `RatFunc.ofFractionRing_injective` states that for any type `K` that has a commutative ring structure, the function `RatFunc.ofFractionRing` is injective. In other words, if this function applied to two elements of `K` gives the same result, then those two elements were actually the same to begin with.
More concisely: If two elements of a commutative ring `K` map to the same element under the function `RatFunc.ofFractionRing`, then those elements are equal in `K`.
|
RatFunc.num_div_dvd'
theorem RatFunc.num_div_dvd' :
∀ {K : Type u} [inst : Field K] (p : Polynomial K) {q : Polynomial K},
q ≠ 0 → Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q) ∣ p
This theorem, `RatFunc.num_div_dvd'`, states that for any field `K` and any polynomials `p` and `q` in that field such that `q` is nonzero, the constant polynomial `Polynomial.C` of the field `K` with the leading coefficient of the ratio of `q` and the greatest common divisor of `p` and `q` as its constant term, all multiplied by the ratio of `p` and the greatest common divisor of `p` and `q`, is a divisor of `p`. In mathematical terms, for all polynomials `p` and `q` (where `q ≠ 0`) in some field `K`, we have
`(Polynomial.C (q / gcd(p, q)).leadingCoeff⁻¹ * (p / gcd(p, q))) ∣ p`
More concisely: For any field `K` and polynomials `p` and `q` (where `q ≠ 0`) in `K`, the constant polynomial obtained by dividing the ratio of `p` and their greatest common divisor by the leading coefficient of the quotient, is a divisor of `p`.
|
RatFunc.num_ne_zero
theorem RatFunc.num_ne_zero : ∀ {K : Type u} [inst : Field K] {x : RatFunc K}, x ≠ 0 → x.num ≠ 0
The theorem `RatFunc.num_ne_zero` states that for any type `K` equipped with a field structure and for any non-zero rational function `x` over this field `K`, the numerator of this rational function, as given by the function `RatFunc.num`, is also non-zero. Essentially, it asserts the non-vanishing property of the numerator for all nonzero rational functions.
More concisely: For any non-zero rational function `x` over a field `K`, its numerator `RatFunc.num x` is non-zero.
|
RatFunc.induction_on'
theorem RatFunc.induction_on' :
∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {P : RatFunc K → Prop} (x : RatFunc K),
(∀ (p q : Polynomial K), q ≠ 0 → P (RatFunc.mk p q)) → P x
This theorem, `RatFunc.induction_on'`, is an induction principle for rational functions (`RatFunc K`). More specifically, it states that if a property `P` holds for all rational functions created by the function `RatFunc.mk` for all polynomials `p` and `q` (where `q` is not equal to zero), then this property `P` holds for all elements of the set of rational functions (`RatFunc K`).
This theorem is particularly useful when we want to prove that a certain property holds for all rational functions. It essentially allows us to reduce the problem to proving that the property holds for all rational functions that can be written in the form `p/q`, where `p` and `q` are polynomials and `q` is non-zero.
Note that there is also a related recursion principle, `induction_on`, which is defined in terms of `algebraMap`.
More concisely: If a property holds for all rational functions `p/q` where `p` and `q` are polynomials with `q ≠ 0`, then it holds for all elements in the set of rational functions `RatFunc K`.
|
RatFunc.mk_eq_div'
theorem RatFunc.mk_eq_div' :
∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (p q : Polynomial K),
RatFunc.mk p q =
{
toFractionRing :=
(algebraMap (Polynomial K) (FractionRing (Polynomial K))) p /
(algebraMap (Polynomial K) (FractionRing (Polynomial K))) q }
The theorem `RatFunc.mk_eq_div'` states that for any commutative ring `K` that is also an integral domain, and any two polynomials `p` and `q` over `K`, the rational function `RatFunc.mk p q` is equal to the fraction where the numerator is the embedding of `p` into the fraction ring of polynomials over `K` and the denominator is the embedding of `q` into the same fraction ring. In other words, `RatFunc.mk p q` is equivalent to the fraction $\frac{\text{{algebraMap}}(p)}{\text{{algebraMap}}(q)}$ in the fraction ring of polynomials over `K`, where $\text{{algebraMap}}$ is the embedding given by the `Algebra` structure.
More concisely: For any commutative integral domain K, the rational function RatFunc.mk p q over K is equal to the fraction of the polynomial embeddings algebraMap(p) and algebraMap(q) in the fraction ring of polynomials over K.
|
RatFunc.induction_on
theorem RatFunc.induction_on :
∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {P : RatFunc K → Prop} (x : RatFunc K),
(∀ (p q : Polynomial K),
q ≠ 0 → P ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q)) →
P x
This theorem, `RatFunc.induction_on`, establishes an induction principle for rational functions over a domain `K`. It asserts that, given any property `P` that applies to elements of rational functions over `K`, if this property holds for any rational function formed by dividing a polynomial `p` by a non-zero polynomial `q` (both from `K`), when these polynomials are mapped from the polynomial ring to the rational function space using the algebra map, then this property `P` holds for all elements of the rational functions over `K`. This theorem is fundamental for proofs involving properties of rational functions.
More concisely: The theorem `RatFunc.induction_on` in Lean 4 asserts that if a property `P` holds for the quotient of two polynomials in a domain `K`, then it holds for all rational functions over `K`.
|