Theorems · Definition · functional analysis

ContinuousLinearEquiv.neg

(R : Type u_1) →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : TopologicalSpace M] → [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → [ContinuousNeg M] → M ≃L[R] M

The negation map as a continuous linear equivalence.

Defined in

Mathlib.Topology.Algebra.Module.Equiv

Cited by

11 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Quot.sound

Assumes

SemiringTopologicalSpaceAddCommGroupModuleContinuousNeg