associated' — Mathlib

English

The ℤ-linear map associated' sends a QuadraticMap to a BilinMap.

Русский

ℤ-линейное отображение associated' переводит квадратичную карту в билинейное отображение.

LaTeX

$$$ associated' : QuadraticMap R M N \to BilinMap R M N $$$

Lean4

/-- `associated'` is the `ℤ`-linear map that sends a quadratic form on a module `M` over `R` to its
associated symmetric bilinear form. -/
abbrev associated' : QuadraticMap R M N →ₗ[ℤ] BilinMap R M N :=
  associatedHom ℤ

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