congr_apply — Mathlib

English

The action of congruence on a bilinear form B by an equivalence e translates to evaluating B on the images under e and its inverse.

Русский

Действие конгруэнции на билинейную форму B через эквивалентность e эквивалентно оценке B на изображения через e и его обратное.

LaTeX

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

Lean4

@[simp]
theorem congr_apply (e : M ≃ₗ[R] M') (B : BilinForm R M) (x y : M') : congr e B x y = B (e.symm x) (e.symm y) :=
  rfl

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