Theorems · Theorem · commutative algebra

algebraMap_injective_of_field_isFractionRing

∀ (R : Type u_1) [inst : CommRing R] (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S] (K : Type u_6)
  (L : Type u_7) [inst_3 : Field K] [inst_4 : Semiring L] [Nontrivial L] [inst_6 : Algebra R K] [IsFractionRing R K]
  [inst_8 : Algebra S L] [inst_9 : Algebra K L] [inst_10 : Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L],
  Function.Injective ⇑(algebraMap R S)

Defined in

Mathlib.RingTheory.Localization.FractionRing

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraFieldSemiringNontrivialAlgebraIsFractionRingAlgebraAlgebraAlgebraIsScalarTowerIsScalarTower