of_mul_of — Mathlib

English

In the free abelian group on α, the embedding of α preserves multiplication: for all x,y ∈ α, of x * of y = of (x * y).

Русский

В свободной абелевой группе на α вложение α в π сохраняет умножение: для всех x,y ∈ α, of x · of y = of (x · y).

LaTeX

$$$\operatorname{of}(x) \cdot \operatorname{of}(y) = \operatorname{of}(x \cdot y)$$$

Lean4

@[simp]
theorem of_mul_of (x y : α) : of x * of y = of (x * y) := by rw [mul_def, lift_apply_of, lift_apply_of]

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