imₗ — Mathlib

English

im acts as a linear map from QuadraticAlgebra to the base ring, i.e., it is a linear functional given by the imaginary part.

Русский

im выступает как линейное отображение из QuadraticAlgebra в базовое кольцо.

LaTeX

$$$\mathrm{im}_\ell : \text{QuadraticAlgebra}(R,a,b) \to R$ is linear with toFun = im$$

Lean4

/-- `QuadraticAlgebra.im` as a `LinearMap` -/
@[simps]
def imₗ : QuadraticAlgebra R a b →ₗ[R] R where
  toFun := im
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

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