quotKerEquivRange_symm_apply_image

English

The object f.quotKerEquivRange sends mk x to f x for all x.

Русский

Объект f.quotKerEquivRange отображает mk x в f(x).

LaTeX

$$theorem quotKerEquivRange_apply_mk (f) (x) : (f.quotKerEquivRange (Submodule.Quotient.mk x) : M₂) = f x$$

Lean4

@[simp]
theorem quotKerEquivRange_symm_apply_image (x : M) (h : f x ∈ LinearMap.range f) :
    f.quotKerEquivRange.symm ⟨f x, h⟩ = (LinearMap.ker f).mkQ x :=
  f.quotKerEquivRange.symm_apply_apply ((LinearMap.ker f).mkQ x)

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