map_smulₛₗ

Mathlib.Algebra.Module.Equiv.Defs

URI: https://scilib.ai/kg/mathlib#LinearEquiv.map_smulₛₗ

English

Let e12: M1 ≃ M2 and f,g: M3 → M2. If f ∘ e12 = g ∘ e12 then f = g.

Русский

Пусть e12: M1 ≃ M2 и f,g: M3 → M2. Если f ∘ e12 = g ∘ e12, то f = g.

LaTeX

$$$ f \circ e_{12} = g \circ e_{12} \Longrightarrow f = g $$$

Lean4

protected theorem map_smulₛₗ (c : R) (x : M) : e (c • x) = (σ : R → S) c • e x :=
  e.map_smul' c x

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru