congrRight₂_trans — Mathlib

English

Applying two congruences in succession is the same as a single congruence with the composed map.

Русский

Наследование двух конгруэнций эквивалентно единой конгруэнции с композиции отображений.

LaTeX

$$congr e (congr f B) = congr (f ∘ e) B$$

Lean4

theorem _root_.LinearEquiv.congrRight₂_trans (e₁₂ : N₁ ≃ₗ[R] N₂) (e₂₃ : N₂ ≃ₗ[R] N₃) :
    LinearEquiv.congrRight₂ (M := M) (e₁₂ ≪≫ₗ e₂₃) = LinearEquiv.congrRight₂ e₁₂ ≪≫ₗ LinearEquiv.congrRight₂ e₂₃ :=
  rfl

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