theorem aux {α : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {f : α → 𝕜} (x : α) : (starRingEnd 𝕜) (f x / ↑‖f x‖) * f x = ↑‖f x‖

theorem enorm_algebraMap' {𝕜 : Type u_1} (𝕜' : Type u_2) [NormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜'] (x : 𝕜) : ‖(algebraMap 𝕜 𝕜') x‖ₑ = ‖x‖ₑ

theorem enorm_integral_starRingEnd_mul_eq_lintegral_enorm {𝕜 : Type u_1} [RCLike 𝕜] {α : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → 𝕜} (hf : MeasureTheory.Integrable f μ) : ‖∫ (x : α), (starRingEnd 𝕜) (f x / ↑‖f x‖) * f x ∂μ‖ₑ = ∫⁻ (x : α), ‖f x‖ₑ ∂μ