coeLinearMap_of — Mathlib

English

The canonical linear map sends the i-th canonical embedding of A_i into x ∈ A_i to x itself in M.

Русский

Каноническое линейное отображение отправляет i-ю инклузию A_i в элемент x в M; результат равен x.

LaTeX

$$$\mathrm{coeLinearMap} A\big(\mathrm(of\ (fun i \mapsto A i) i) \, x\big) = x.$$$

Lean4

@[simp]
theorem coeLinearMap_of (i : ι) (x : A i) : DirectSum.coeLinearMap A (of (fun i ↦ A i) i x) = x :=
  -- Porting note: spelled out arguments. (I don't know how this works.)

  toAddMonoid_of (β := fun i => A i) (fun i ↦ ((A i).subtype : A i →+ M)) i x

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