Theorems · Definition · functional analysis

DilationEquiv.smulTorsor

{𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : NormedDivisionRing 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] →
        [inst_2 : Module 𝕜 E] →
          [NormSMulClass 𝕜 E] →
            {P : Type u_3} → [inst_4 : PseudoMetricSpace P] → [NormedAddTorsor E P] → P → {k : 𝕜} → k ≠ 0 → E ≃ᵈ P

Scaling by an element k of the scalar ring as a DilationEquiv with ratio ‖k‖₊, mapping from a normed space to a normed torsor over that space sending 0 to c.

Defined in

Mathlib.Analysis.Normed.Affine.AddTorsor

Cited by

5 results in Mathlib

Foundations

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

Assumes

NormedDivisionRingSeminormedAddCommGroupModuleNormSMulClassPseudoMetricSpaceNormedAddTorsor