mk_coe' — Mathlib

English

The underlying additive map of a σ-linear map f, when reassembled via the constructor mk with its corresponding additive data, yields f again; i.e., (mk f.toAddHom h) = f.

Русский

У подлежащего σ-линейного отображения f, взятого через конструктор mk с соответствующими аддитивными данными, получается обратно f; тождество (mk f.toAddHom h) = f.

LaTeX

$$$ (\mathrm{mk} \ f.\!toAddHom \ h) = f $$$

Lean4

@[simp]
theorem mk_coe' (f : M →ₛₗ[σ] M₃) (h) : (mk f.toAddHom h : M →ₛₗ[σ] M₃) = f :=
  rfl

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