Theorems · Definition · commutative algebra

Module.Basis.smulTower

{R : Type u_1} →
  {S : Type u_2} →
    {A : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          [inst_2 : AddCommMonoid A] →
            [inst_3 : Module R S] →
              [inst_4 : Module S A] →
                [inst_5 : Module R A] →
                  [IsScalarTower R S A] →
                    {ι : Type u_5} →
                      {ι' : Type u_6} → Module.Basis ι R S → Module.Basis ι' S A → Module.Basis (ι × ι') R A

Basis.smulTower (b : Basis ι R S) (c : Basis ι S A) is the R-basis on A where the (i, j)th basis vector is b i • c j.

Defined in

Mathlib.RingTheory.AlgebraTower

Cited by

13 results in Mathlib

Foundations

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

Assumes

SemiringSemiringAddCommMonoidModuleModuleModuleIsScalarTower