Theorems · Theorem · field theory

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

Defined in

Mathlib.FieldTheory.RatFunc.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainCommGroupWithZero