mul_def — Mathlib

English

Let α be a type with a multiplicative operation. In the free abelian group on α, the product x ⋅ y is defined by x ⋅ y = lift (λ x₂ ↦ lift (λ x₁ ↦ of (x₁ · x₂)) x) y.

Русский

Пусть α — множество с умножением. В свободной абелевой группе на α произведение x · y задаётся как x · y = lift (λ x₂ ↦ lift (λ x₁ ↦ of (x₁ · x₂)) x) y.

LaTeX

$$$ x \\cdot y = \\mathrm{lift}\\bigl(\\lambda x_2 \\mapsto \\mathrm{lift}(\\lambda x_1 \\mapsto \\mathrm{of}(x_1 \\cdot x_2))\\ x\\bigr)\\ y $$$

Lean4

theorem mul_def (x y : FreeAbelianGroup α) : x * y = lift (fun x₂ ↦ lift (fun x₁ ↦ of (x₁ * x₂)) x) y :=
  rfl

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