funCongrLeft_comp — Mathlib

English

Conjugation of congrLeft by composed equivalences equals the composition of congrLefts in the opposite order: funCongrLeft(R,M,(e1.trans e2)) = (funCongrLeft(R,M,e2)).trans (funCongrLeft(R,M,e1)).

Русский

Сопряжение конглев слева по объединенным эквивалентностям равно композиции конглев слева в обратном порядке.

LaTeX

$$$ \mathrm{funCongrLeft}\; R\; M\; (e_1.trans\; e_2) = (\mathrm{funCongrLeft}\; R\; M\; e_2).\mathrm{trans} (\mathrm{funCongrLeft}\; R\; M\; e_1) $$$

Lean4

@[simp]
theorem funCongrLeft_comp (e₁ : m ≃ n) (e₂ : n ≃ p) :
    funCongrLeft R M (Equiv.trans e₁ e₂) = LinearEquiv.trans (funCongrLeft R M e₂) (funCongrLeft R M e₁) :=
  rfl

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