val_smul_of_tower — Mathlib

English

Let p be a SubMulAction of M over a scalar tower S → R → M. Then the S-action on p agrees with the ambient S-action on M when p is viewed inside M; i.e., for every s ∈ S and every x ∈ p, the element (s · x) taken as an element of M equals s · (x taken as an element of M).

Русский

Пусть p — SubMulAction над M в рамках скалярной башни S → R → M. Тогда действие S на p по ограничению совпадает с действием S на M: для всякого s ∈ S и x ∈ p верно, что (s · x) как элемент p, рассматриваться как элемент M, равен s · (x как элемент M).

LaTeX

$$$ \\forall s : S, \\forall x : p,\\ ((s \\cdot x) : M) = s \\cdot (x : M). $$$

Lean4

@[to_additive (attr := norm_cast, simp)]
theorem val_smul_of_tower (s : S) (x : p) : ((s • x : p) : M) = s • (x : M) :=
  rfl

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