Theorems · Definition · commutative algebra

IsFractionRing.mulSemiringAction

(G : Type u_10) →
  (B : Type u_12) →
    (L : Type u_14) →
      [inst : Group G] →
        [inst_1 : CommRing B] →
          [MulSemiringAction G B] →
            [inst_3 : Field L] → [inst_4 : Algebra B L] → [IsFractionRing B L] → MulSemiringAction G L

Given a MulSemiringAction G B, extend the action of G on B to a MulSemiringAction G L on the fraction field L of B.

Defined in

Mathlib.RingTheory.Localization.FractionRing

Cited by

4 results in Mathlib

Foundations

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

Assumes

GroupCommRingMulSemiringActionFieldAlgebraIsFractionRing