flip — Mathlib

English

Let B be a bilinear form on an R-module M. Its flip, denoted B^flip, is the bilinear form obtained by swapping the two arguments, i.e., (B^flip)(x,y) = B(y,x) for all x,y in M.

Русский

Пусть B — билинейная форма над модулем M над кольцом R. Ее переворот B^flip получается путём обмена аргументов: (B^flip)(x, y) = B(y, x) для всех x, y ∈ M.

LaTeX

$$$$ (B^{\mathrm{flip}})(x,y)=B(y,x) \quad\text{for all } x,y \in M. $$$$

Lean4

/-- The `flip` of a bilinear form over a commutative ring, obtained by exchanging the left and
right arguments. -/
abbrev flip (B : BilinForm R M) :=
  flipHom B

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