coe_smul

Mathlib.Topology.Algebra.Module.Alternating.Basic

URI: https://scilib.ai/kg/mathlib#ContinuousAlternatingMap.coe_smul

English

Coercion to function commutes with scalar multiplication for continuous alternating maps.

Русский

Преобразование в функцию commuting со скалярным умножением для непрерывных чередующихся отображений.

LaTeX

$$$$\\text{coe}(c \\cdot f) = c \\cdot \\text{coe}(f).$$$$

Lean4

@[simp]
theorem coe_smul (f : M [⋀^ι]→L[A] N) (c : R') : ⇑(c • f) = c • ⇑f :=
  rfl

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

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

Разделы

Аффилиация

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