isIdempotentElem_toLinearMap_iff — Mathlib

English

For a continuous linear map f, f is idempotent iff its underlying linear map is idempotent.

Русский

Для непрерывно-линейного отображения f выполняется: f идемпотентно тогда и только тогда, когда его базовая линейная карта идемпотентна.

LaTeX

$$$\text{IsIdempotentElem}(f) \;\Longleftrightarrow\; \text{IsIdempotentElem}(f^{\text{toLinearMap}})$$$

Lean4

@[grind =]
theorem isIdempotentElem_toLinearMap_iff {R M : Type*} [Semiring R] [TopologicalSpace M] [AddCommMonoid M] [Module R M]
    {f : M →L[R] M} : IsIdempotentElem f.toLinearMap ↔ IsIdempotentElem f := by
  simp only [IsIdempotentElem, Module.End.mul_eq_comp, ← coe_comp, mul_def, coe_inj]

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