toDual_mul

Mathlib.Algebra.Order.Group.Synonym

URI: https://scilib.ai/kg/mathlib#toDual_mul

English

The dual map preserves multiplication: for all a,b in α, toDual(a b) = toDual(a) toDual(b).

Русский

Двойственное отображение сохраняет умножение: для всех a,b ∈ α выполняется toDual(a b) = toDual(a) toDual(b).

LaTeX

$$$ toDual(a b) = toDual(a) \cdot toDual(b) $$$

Lean4

@[to_additive (attr := simp)]
theorem toDual_mul [Mul α] (a b : α) : toDual (a * b) = toDual a * toDual b :=
  rfl

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

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

Разделы

Аффилиация

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