English
For a linear isometry f, the property IsSymmetric is preserved under conjugation equivalence, i.e., is symmetric iff the transported operator is symmetric.
Русский
Для линейного изометрического отображения f свойство симметричности сохраняется при переносе оператора через сопряжение-изоморфизм: симметрично тогда и только тогда, когда преобразованный оператор симметричен.
LaTeX
$$$ isSymmetric\_linearIsometryEquiv\_conj\_iff \; (T : E \to E) (f : E \to_{op} F) : (f \circ T \circ f^{-1}).IsSymmetric \iff T.IsSymmetric $$$
Lean4
theorem isSymmetric_linearIsometryEquiv_conj_iff {F : Type*} [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F]
(T : E →ₗ[𝕜] E) (f : E ≃ₗᵢ[𝕜] F) : (f.toLinearMap ∘ₗ T ∘ₗ f.symm.toLinearMap).IsSymmetric ↔ T.IsSymmetric :=
by
refine ⟨fun h x y => ?_, fun h x y => ?_⟩
· simpa [LinearIsometryEquiv.inner_map_eq_flip] using h (f x) (f y)
· simp [LinearIsometryEquiv.inner_map_eq_flip, h _ (f.symm y)]
