congr — Mathlib

English

Applying congruence with e then f is the same as congruence with the composition f ∘ e on the bilinear form B.

Русский

Применение конгруэнции сначала по e, затем по f эквивалентно конгруэнции по композиции f ∘ e на билинейной форме B.

LaTeX

$$$ congr\, e\\, (congr\\, f\\, B) = congr\\,(f \\circ e)\, B $$$

Lean4

/-- Apply a linear equivalence on the arguments of a bilinear form. -/
def congr (e : M ≃ₗ[R] M') : BilinForm R M ≃ₗ[R] BilinForm R M' :=
  LinearEquiv.congrRight (LinearEquiv.congrLeft _ _ e) ≪≫ₗ LinearEquiv.congrLeft _ _ e

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