Theorems · Theorem · field theory

RatFunc.map_apply

∀ {K : Type u} [inst : Field K] {R : Type u_1} {F : Type u_2} [inst_1 : CommRing R] [inst_2 : IsDomain R]
  [inst_3 : FunLike F (Polynomial K) (Polynomial R)] [inst_4 : MonoidHomClass F (Polynomial K) (Polynomial R)] (φ : F)
  (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial R))) (f : RatFunc K),
  (RatFunc.map φ hφ) f =
    (algebraMap (Polynomial R) (RatFunc R)) (φ f.num) / (algebraMap (Polynomial R) (RatFunc R)) (φ f.denom)

Defined in

Mathlib.FieldTheory.RatFunc.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldCommRingIsDomainFunLikeMonoidHomClass