comp_congr — Mathlib

English

Congruence commutes with composition of maps: (congr e B).comp l r equals B.comp (e.symm ∘ l) (e.symm ∘ r).

Русский

Согласование совместимо с композицией отображений: (congr e B).comp l r = B.comp (e.symm ∘ l) (e.symm ∘ r).

LaTeX

$$((congr e) B).comp l r = B.comp (e.symm ∘ l) (e.symm ∘ r)$$

Lean4

theorem comp_congr (e : M' ≃ₗ[R] M'') (B : BilinForm R M) (l r : M' →ₗ[R] M) :
    congr e (B.comp l r) = B.comp (l.comp (e.symm : M'' →ₗ[R] M')) (r.comp (e.symm : M'' →ₗ[R] M')) :=
  rfl

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