congrLinearEquiv_apply — Mathlib

English

For e12: M1 ≃ₛₗ[σ12] M2 and g ∈ GeneralLinearGroup R1 M1, the image under congrLinearEquiv is the element of GeneralLinearGroup R2 M2 corresponding to the linear conjugation e12.symm.trans (g.toLinearEquiv.trans e12).

Русский

Для e12: M1 ≃ₛₗ[σ12] M2 и g ∈ GeneralLinearGroup R1 M1 образ под congrLinearEquiv есть элемент в GeneralLinearGroup R2 M2, соответствующий линейному сопряжению e12.symm.trans (g.toLinearEquiv.trans e12).

LaTeX

$$$ congrLinearEquiv e_{12} \, g = \text{ofLinearEquiv}(e_{12}^{\mathsf{symm}} \;\circ\; g^{\;toLinearEquiv} \;\circ\; e_{12}). $$$

Lean4

@[simp]
theorem congrLinearEquiv_apply (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (g : GeneralLinearGroup R₁ M₁) :
    congrLinearEquiv e₁₂ g = ofLinearEquiv (e₁₂.symm.trans <| g.toLinearEquiv.trans e₁₂) :=
  rfl

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