ofFinsupp_add — Mathlib

English

In SkewMonoidAlgebra, the image of a + b equals the sum of the images of a and b: ⟨a + b⟩ = ⟨a⟩ + ⟨b⟩.

Русский

В SkewMonoidAlgebra отображение ⟨·⟩ сохраняет сложение: ⟨a + b⟩ = ⟨a⟩ + ⟨b⟩.

LaTeX

$$$ (\langle a + b \rangle : SkewMonoidAlgebra k G) = \langle a \rangle + \langle b \rangle $$$

Lean4

@[simp]
theorem ofFinsupp_add {a b} : (⟨a + b⟩ : SkewMonoidAlgebra k G) = ⟨a⟩ + ⟨b⟩ :=
  show _ = add _ _ by rw [add]

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