congrLinearEquiv_trans' — Mathlib

English

A stronger form of congrLinearEquiv.trans for semilinear maps; equality holds in full generality when composing via trans.

Русский

Усиленная форма congrLinearEquiv.trans для семилинейных отображений; равенство сохраняется в полной общности при композиции через trans.

LaTeX

$$$ (congrLinearEquiv e_{12}).trans (congrLinearEquiv e_{23}) = congrLinearEquiv (e_{12}.trans e_{23}) $$$

Lean4

/-- Stronger form of `congrLinearEquiv.trans` applying to semilinear maps. Not a simp lemma as
`σ₁₃` and `σ₃₁` cannot be inferred from the LHS. -/
theorem congrLinearEquiv_trans' (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃) :
    (congrLinearEquiv e₁₂).trans (congrLinearEquiv e₂₃) = congrLinearEquiv (e₁₂.trans e₂₃) :=
  rfl

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