Theorems · Definition · field theory

RatFunc.liftAlgebra

(R : Type u_1) →
  (L : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : Field L] →
        [inst_2 : IsDomain R] →
          [inst_3 : Algebra (Polynomial R) L] → [FaithfulSMul (Polynomial R) L] → Algebra (RatFunc R) L

FractionRing.liftAlgebra specialized to R⟮X⟯. This is a scoped instance because it creates a diamond when L = R⟮X⟯.

Defined in

Mathlib.FieldTheory.RatFunc.Basic

Cited by

15 results in Mathlib

Foundations

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

Assumes

CommRingFieldIsDomainAlgebraFaithfulSMul