Theorems · Theorem · functional analysis

ContinuousLinearMap.IsIdempotentElem.commute_iff_of_isUnit

∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : IsTopologicalAddGroup M] {f T : M →L[R] M},
  IsUnit T →
    IsIdempotentElem f →
      (Commute f T ↔ Submodule.map (↑T) (↑f).range = (↑f).range ∧ Submodule.map (↑T) (↑f).ker = (↑f).ker)

An idempotent operator f commutes with a unit operator T if and only if T (range f) = range f and T (ker f) = ker f.

Defined in

Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent

Cited by

0 results in Mathlib

Foundations

Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingTopologicalSpaceAddCommGroupModuleIsTopologicalAddGroup