Theorems · Theorem · field theory

RatFunc.liftAlgHom_apply_div

∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {L : Type u_1} {S : Type u_3} [inst_2 : Field L]
  [inst_3 : CommSemiring S] [inst_4 : Algebra S (Polynomial K)] [inst_5 : Algebra S L] (φ : Polynomial K →ₐ[S] L)
  (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (p q : Polynomial K),
  (RatFunc.liftAlgHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) =
    φ p / φ q

Defined in

Mathlib.FieldTheory.RatFunc.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainFieldCommSemiringAlgebraAlgebra