coe_isComplEquivProj_symm_apply — Mathlib

English

The kernel of the projection inverse under IsComplEquivProj equals the corresponding Submodule ker, i.e., the kernel of f is the submodule obtained from the symm image.

Русский

Ядро проекции в обратном образе при IsComplEquivProj совпадает с ядром соответствующего отображения.

LaTeX

$$$ (p.isComplEquivProj.symm\ f\;: E \to p)\;\text{as Submodule} = \ker(f). $$$

Lean4

@[simp]
theorem coe_isComplEquivProj_symm_apply (f : { f : E →ₗ[R] p // ∀ x : p, f x = x }) :
    (p.isComplEquivProj.symm f : Submodule R E) = ker (f : E →ₗ[R] p) :=
  rfl

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