theorem starRingEnd_div_mul_eq_norm {α : 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_norm_eq_integral_enorm {α : Type u_1} {𝕜 : Type u_2} [MeasurableSpace α] [RCLike 𝕜] {μ : MeasureTheory.Measure α} {f : α → 𝕜} (hf : MeasureTheory.Integrable f μ) : ‖∫ (x : α), ‖f x‖ ∂μ‖ₑ = ∫⁻ (x : α), ‖f 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‖ₑ ∂μ

theorem enorm_integral_mul_starRingEnd_comm {𝕜 : Type u_1} [RCLike 𝕜] {α : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → 𝕜} : ‖∫ (x : α), f x * (starRingEnd 𝕜) (g x) ∂μ‖ₑ = ‖∫ (x : α), g x * (starRingEnd 𝕜) (f x) ∂μ‖ₑ