comp_eq_left_iff — Mathlib

English

Let q be idempotent. For p, p ∘ q = p if and only if ker q ≤ ker p.

Русский

Пусть q идемпотент. Тогда p ∘ q = p тогда и только тогда, когда ker q ⊆ ker p.

LaTeX

$$$ p \circ q = p \iff \ker(q) \le \ker(p) $$$

Lean4

theorem comp_eq_left_iff {M : Type*} [AddCommGroup M] [Module S M] {q : M →ₗ[S] M} (hq : IsIdempotentElem q) {E : Type*}
    [AddCommGroup E] [Module S E] (p : M →ₗ[S] E) : p ∘ₗ q = p ↔ ker q ≤ ker p := by
  simp [hq.ker_eq_range, range_le_ker_iff, comp_sub, Module.End.one_eq_id, sub_eq_zero, eq_comm (a := p)]

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