of_isScalarTower — Mathlib

English

If M,N α satisfy a scalar tower and M α is pretransitive, then N α is pretransitive.

Русский

Если существует тензор скаляров M→N→α и M действует предпереставимо на α, тогда N действует предпереставимо на α.

LaTeX

$$$\\text{IsScalarTower } M N α \\text{ и } \\text{MulAction.IsPretransitive } M α \\Rightarrow \\text{IsPretransitive } N α$$$

Lean4

@[to_additive]
theorem of_isScalarTower (M : Type*) {N α : Type*} [Monoid N] [SMul M N] [MulAction N α] [SMul M α]
    [IsScalarTower M N α] [IsPretransitive M α] : IsPretransitive N α :=
  of_smul_eq (fun x : M ↦ x • 1) (smul_one_smul N _ _)

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