congr_trans — Mathlib

English

The congruence of a pair of composed linear equivalences equals the composition of the congruences: congr (f ≪≫ f') (g ≪≫ g') = congr f g ≪≫ congr f' g'.

Русский

Сопоставление через композицию равняется композиции сопоставлений: cong (f ∘ f') (g ∘ g') = cong f g ∘ cong f' g'.

LaTeX

$$$ congr\\ (f \\circ f')\\ (g \\circ g') = (congr f g) \\circ (congr f' g') $$$

Lean4

theorem congr_trans (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (f' : P ≃ₗ[R] S) (g' : Q ≃ₗ[R] T) :
    congr (f ≪≫ₗ f') (g ≪≫ₗ g') = congr f g ≪≫ₗ congr f' g' :=
  LinearEquiv.toLinearMap_injective <| map_comp _ _ _ _

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