Theorems · Theorem · field theory

RatFunc.numDenom_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).numDenom =
      (Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q),
        Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q))

Defined in

Mathlib.FieldTheory.RatFunc.Basic

Cited by

1 results in Mathlib

Foundations

Depth 127 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Field