Theorems · Definition · functional analysis

ContinuousLinearEquiv.restrictScalars

(R : Type u_1) →
  {S : Type u_2} →
    {M : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Module R M] →
              [inst_4 : Module S M] →
                [inst_5 : TopologicalSpace M] → [LinearMap.CompatibleSMul M M R S] → (M ≃L[S] M) → M ≃L[R] M

If M is an R-module and S-module and R-module structure is defined by an action of R on S (formally, we have two scalar towers), then any S-linear equivalence on M is an R-linear equivalence.

Defined in

Mathlib.Topology.Algebra.Module.Equiv

Cited by

3 results in Mathlib

Foundations

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

Assumes

SemiringSemiringAddCommMonoidModuleModuleTopologicalSpaceLinearMap.CompatibleSMul