congrQuadraticMap_symm — Mathlib

English

For any isomorphism e, the inverse of the induced congrQuadraticMap corresponds to conjugation by e^{-1}: (congrQuadraticMap e).symm = e.symm.congrQuadraticMap.

Русский

Для изomорфизма e обратимое отображение между пространствами квадратичных отображений соответствует сопряжению через e^{-1}.

LaTeX

$$$(LinearEquiv.congrQuadraticMap\ e).symm = e^{-1}.congrQuadraticMap$.$$

Lean4

@[simp]
theorem _root_.LinearEquiv.congrQuadraticMap_symm (e : N ≃ₗ[R] P) :
    (LinearEquiv.congrQuadraticMap e (M := M)).symm = e.symm.congrQuadraticMap :=
  rfl

Похожие утверждения