coe_smul — Mathlib

English

Let S be an intermediate field of L over K. For any R with compatible scalar actions and any r ∈ R and x ∈ S, the inclusion map i: S → L is R-linear, i(r · x) = r · i(x).

Русский

Пусть S — промежуточное поле L над K. Пусть R действует совместимо со скалярами K и L, и возьмем любой r ∈ R и x ∈ S. Тогда включение i: S → L удовлетворяет i(r · x) = r · i(x).

LaTeX

$$$\\iota_S(r x) = r\\,\\iota_S(x) \\quad (r \\in R,\\ x \\in S)$$$

Lean4

@[simp]
theorem coe_smul {R} [SMul R K] [SMul R L] [IsScalarTower R K L] (r : R) (x : S) : ↑(r • x : S) = (r • (x : L)) :=
  rfl

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