map_mul

Mathlib.Topology.Algebra.PontryaginDual

URI: https://scilib.ai/kg/mathlib#PontryaginDual.map_mul

English

The dualization map is compatible with multiplication: map(f * g) = map f * map g.

Русский

Дуализация сохраняет умножение: map(f·g) = map f · map g.

LaTeX

$$$\\text{map}(f \\cdot g) = \\text{map}(f) \\cdot \\text{map}(g)$$$

Lean4

@[simp]
nonrec theorem map_mul (f g : A →ₜ* G) : map (f * g) = map f * map g :=
  ext fun x => ext fun y => map_mul x (f y) (g y)

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

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

Разделы

Аффилиация

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