isScalarTower_iff_smulCommClass_of_commMonoid

English

Let R1 and R be as above with R commutative. Then SMulCommClass R1 R R if and only if IsScalarTower R1 R R.

Русский

Пусть R1 и R имеют такие же условия, что и ранее, причем R коммутативен. Тогда SMulCommClass R1 R R эквивалентно IsScalarTower R1 R R.

LaTeX

$$$ \text{SMulCommClass } R1\ R\ R \iff \text{IsScalarTower } R1\ R\ R $$$

Lean4

theorem isScalarTower_iff_smulCommClass_of_commMonoid (R₁ R : Type*) [Monoid R₁] [CommMonoid R] [MulAction R₁ R] :
    SMulCommClass R₁ R R ↔ IsScalarTower R₁ R R :=
  ⟨fun _ ↦ IsScalarTower.of_commMonoid R₁ R, fun _ ↦ SMulCommClass.of_commMonoid R₁ R R⟩

Похожие утверждения