Theorems · Definition · commutative algebra

Module.Presentation.RestrictScalarsData

{B : Type u_1} →
  [inst : Ring B] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module B M] →
          [DecidableEq B] →
            (presM : Module.Presentation B M) →
              [DecidableEq presM.G] →
                {A : Type u_3} →
                  [inst_5 : CommRing A] →
                    [inst_6 : Algebra A B] → Module.Presentation A B → Type (max (max (max u_3 u_6) u_4) u_6 u_5)

The additional data that is necessary in order to obtain a presentation of the restriction of scalars of a module.

Defined in

Mathlib.Algebra.Module.Presentation.RestrictScalars

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupModuleDecidableEqDecidableEqCommRingAlgebra