Rescaling continuous linear equivalences

A continuous linear equivalence T : E ≃L[𝕜] F over a field can be multiplied by a nonzero scalar d; the result is again a continuous linear equivalence, whose inverse is d⁻¹ • T⁻¹. The construction uses Mathlib's ContinuousLinearEquiv.equivOfInverse'.

Dually, multiplying a continuous linear map by a nonzero scalar c is composing it with the scalar equivalence ContinuousLinearEquiv.smulLeft (Units.mk0 c hc), so results about composition with equivalences apply to scalar multiples.

theorem ContinuousLinearEquiv.exists_coe_eq_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Field 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousConstSMul 𝕜 E] [ContinuousConstSMul 𝕜 F] (T : E ≃L[𝕜] F) {d : 𝕜} (hd : d ≠ 0) : ∃ (U : E ≃L[𝕜] F), ↑U = d • ↑T ∧ ↑U.symm = d⁻¹ • ↑T.symm

Rescaling a continuous linear equivalence by a nonzero scalar d gives a continuous linear equivalence, whose inverse is the inverse rescaled by d⁻¹.

theorem ContinuousLinearMap.smul_eq_smulLeft_comp {𝕜 : Type u_1} {M : Type u_2} {M₂ : Type u_3} [Field 𝕜] [TopologicalSpace M] [AddCommMonoid M] [Module 𝕜 M] [TopologicalSpace M₂] [AddCommMonoid M₂] [Module 𝕜 M₂] [ContinuousConstSMul 𝕜 M₂] {c : 𝕜} (hc : c ≠ 0) (f : M →L[𝕜] M₂) : c • f = ↑(ContinuousLinearEquiv.smulLeft (Units.mk0 c hc)) ∘SL f

Multiplying by a nonzero scalar is composing with the corresponding scalar equivalence.