Theorems · Definition · functional analysis

LinearEquiv.withLpCongr

(p : ENNReal) →
  {K : Type u_1} →
    {K' : Type u_2} →
      {V : Type u_4} →
        {V' : Type u_5} →
          [inst : Semiring K] →
            [inst_1 : Semiring K'] →
              {σ : K →+* K'} →
                {σ' : K' →+* K} →
                  [inst_2 : RingHomInvPair σ σ'] →
                    [inst_3 : RingHomInvPair σ' σ] →
                      [inst_4 : AddCommGroup V] →
                        [inst_5 : Module K V] →
                          [inst_6 : AddCommGroup V'] →
                            [inst_7 : Module K' V'] → (V ≃ₛₗ[σ] V') → WithLp p V ≃ₛₗ[σ] WithLp p V'

Lift a (semi)linear equivalence to WithLp.

Defined in

Mathlib.Analysis.Normed.Lp.WithLp

Cited by

4 results in Mathlib

Foundations

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

Assumes

SemiringSemiringRingHomInvPairRingHomInvPairAddCommGroupModuleAddCommGroupModule