ofDual_mul — Mathlib

English

The OfDual map from the dual to the original preserves multiplication: for all a,b in αᵒᵈ, ofDual(a b) = ofDual(a) ofDual(b).

Русский

Отображение OfDual из двойственного объекта в исходный сохраняет умножение: for a,b ∈ αᵒᵈ, ofDual(a b) = ofDual(a) ofDual(b).

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem ofDual_mul [Mul α] (a b : αᵒᵈ) : ofDual (a * b) = ofDual a * ofDual b :=
  rfl

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