Theorems · Theorem · commutative algebra

IsFractionRing.faithfulSMul

∀ (G : Type u_10) (B : Type u_12) (L : Type u_14) [inst : Group G] [inst_1 : CommRing B]
  [inst_2 : MulSemiringAction G B] [inst_3 : Field L] [inst_4 : Algebra B L] [IsFractionRing B L]
  [inst_6 : MulSemiringAction G L] [SMulDistribClass G B L] [FaithfulSMul G B], FaithfulSMul G L

Defined in

Mathlib.RingTheory.Localization.FractionRing

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupCommRingMulSemiringActionFieldAlgebraIsFractionRingMulSemiringActionSMulDistribClassFaithfulSMul