𝕜 : Type u_1
E : Type ?u.606441
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x y : F
⊢ ↑re (inner y x * ↑(starRingEnd 𝕜) (inner y x)) = ‖inner y x * ↑(starRingEnd 𝕜) (inner y x)‖
𝕜 : Type u_1
E : Type ?u.606441
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x y : F
⊢ ↑re (inner x y * inner y x) = ‖inner x y * inner y x‖
rw [← inner_conj_symm, mul_comm]
no goals
𝕜 : Type u_1
E : Type ?u.606441
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x y : F
⊢ ↑re (inner y x * ↑(starRingEnd 𝕜) (inner y x)) = ‖inner y x * ↑(starRingEnd 𝕜) (inner y x)‖
exact re_eq_norm_of_mul_conj (inner y x)