Theorems · Definition · commutative algebra

FractionRing.liftAlgebra

(R : Type u_1) →
  [inst : CommRing R] →
    (K : Type u_5) → [inst_1 : Field K] → [inst_2 : Algebra R K] → [FaithfulSMul R K] → Algebra (FractionRing R) K

This is not an instance because it creates a diamond when K = FractionRing R. Should usually be introduced locally along with isScalarTower_liftAlgebra See note [reducible non-instances].

Defined in

Mathlib.RingTheory.Localization.FractionRing

Cited by

43 results in Mathlib

Foundations

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

Assumes

CommRingFieldAlgebraFaithfulSMul