ext_iff — Mathlib

English

Two idempotent endomorphisms are equal iff they have the same range and the same kernel.

Русский

Два идемпотентных эндоморфизма равны тогда и только тогда, когда совпадают их образы и ядра.

LaTeX

$$$\text{IsIdempotentElem}(p) \land \text{IsIdempotentElem}(q) \Rightarrow (p=q) \iff (\operatorname{range} p = \operatorname{range} q) \land (\ker p = \ker q)$$$

Lean4

/-- Idempotent operators are equal iff their range and kernels are. -/
theorem ext_iff {p q : M →L[R] M} (hp : IsIdempotentElem p) (hq : IsIdempotentElem q) :
    p = q ↔ range p = range q ∧ ker p = ker q := by
  simpa using LinearMap.IsIdempotentElem.ext_iff hp.toLinearMap hq.toLinearMap

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