congr_comp — Mathlib

English

Applying congruence to B by e and then applying the result to x,y is equivalent to applying B to e.symm x and e.symm y.

Русский

Применение конгруэнции к B через e затем к x,y эквивалентно применению B к e.symm x и e.symm y.

LaTeX

$$congr e B x y = B (e.symm x) (e.symm y)$$

Lean4

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

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