Theorems · Theorem · field theory

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)

Defined in

Mathlib.FieldTheory.RatFunc.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

Field