splitMul_apply — Mathlib

English

In Unitization 𝕜 A, the splitMul map evaluates to the pair consisting of the first component and the sum of the linear map corresponding to the first component and the multiplication by the second component.

Русский

В Unitization 𝕜 A отображение splitMul оценивает элемент в пару: первый компонент и сумму отображения, соответствующего первому компоненту, с умножением на второй компонент.

LaTeX

$$$$splitMul\\, 𝕜 A\\, x = \\bigl(x.fst,\\ algebraMap\\ 𝕜 (A \\to_L[𝕜] A)\\, x.fst + mul\\ 𝕜 A\\, x.snd\\bigr).$$$$

Lean4

@[simp]
theorem splitMul_apply (x : Unitization 𝕜 A) :
    splitMul 𝕜 A x = (x.fst, algebraMap 𝕜 (A →L[𝕜] A) x.fst + mul 𝕜 A x.snd) :=
  show (x.fst + 0, _) = (x.fst, _) by rw [add_zero]; rfl

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