Theorems · Definition · functional analysis

Submodule.ClosedComplemented

{R : Type u_1} →
  [inst : Ring R] →
    {M : Type u_2} → [TopologicalSpace M] → [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → Submodule R M → Prop

A submodule p is called complemented if there exists a continuous projection M →ₗ[R] p.

Defined in

Mathlib.Topology.Algebra.Module.Complement

Cited by

40 results in Mathlib

Foundations

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

Assumes

RingTopologicalSpaceAddCommGroupModule