Theorems · Theorem · field theory

RatFunc.map_apply_div

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

Defined in

Mathlib.FieldTheory.RatFunc.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainCommRingIsDomainFunLikeMonoidWithZeroHomClass