of_smul_one_mul — Mathlib

English

Let M, N, P, Q be types with SMul actions such that M ⟶ N, M ⟶ P, M ⟶ Q, N ⟶ P, N ⟶ Q, and P ⟶ Q towers hold; then there is a scalar tower M ⟶ N ⟶ Q.

Русский

Пусть M, N, P, Q имеют действия скаляров и существуют башни M→N, N→P, P→Q и т. д.; тогда существует башня M→N→Q.

LaTeX

$$$ \text{IsScalarTower } M N Q$$$

Lean4

@[to_additive]
theorem of_smul_one_mul {M N} [Monoid N] [SMul M N] (h : ∀ (x : M) (y : N), x • (1 : N) * y = x • y) :
    IsScalarTower M N N :=
  ⟨fun x y z ↦ by rw [← h, smul_eq_mul, mul_assoc, h, smul_eq_mul]⟩

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