Theorems · Theorem · functional analysis

ContinuousLinearMap.inverse_id

∀ {R : Type u_1} {M : Type u_2} [inst : TopologicalSpace M] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M], (ContinuousLinearMap.id R M).inverse = ContinuousLinearMap.id R M

Defined in

Mathlib.Topology.Algebra.Module.Equiv

Cited by

6 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceSemiringAddCommMonoidModule