Theorems · Theorem · field theory

RatFunc.liftMonoidWithZeroHom_apply

∀ {K : Type u} [inst : Field K] {L : Type u_1} [inst_1 : CommGroupWithZero L] (φ : Polynomial K →*₀ L)
  (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (f : RatFunc K),
  (RatFunc.liftMonoidWithZeroHom φ hφ) f = φ f.num / φ f.denom

Defined in

Mathlib.FieldTheory.RatFunc.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldCommGroupWithZero