LinearEquiv.toSpanNonzeroSingleton_homothety

theorem LinearEquiv.toSpanNonzeroSingleton_homothety : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : BoundedSMul 𝕜 E] (x : E) (h : x ≠ 0) (c : 𝕜), ‖(LinearEquiv.toSpanNonzeroSingleton 𝕜 E x h) c‖ = ‖x‖ * ‖c‖

This theorem states that for any type 𝕜, normed division ring over 𝕜, seminormed additive commutative group E, a module 𝕜 E, a bounded scalar multiplication of 𝕜 and E, and any non-zero element x of E, and any element c of 𝕜, the norm of the element obtained by applying the linear equivalence `toSpanNonzeroSingleton` with arguments 𝕜, E, x, h (where h is the condition that x ≠ 0) to the element c, is equal to the product of the norm of x and the norm of c. This theorem can be understood as stating the property that the norm of the projection of an element c in the span of a non-zero element x is proportional to the norm of x and the norm of c.

More concisely: For any normed division ring 𝕜, seminormed additive commutative group E, module 𝕜 E, and bounded scalar multiplication, the norm of the product of a non-zero element x in E and any scalar c in 𝕜, as defined by `toSpanNonzeroSingleton`, equals the product of the norms of x and c.