funLeft — Mathlib

English

Conjugating the identity map by any linear equivalence yields the identity map on the target space: (e.conj Id) = Id.

Русский

Сопряжение тождественного отображения любым линейным эквивелентом даёт тождественное отображение в целевом пространстве.

LaTeX

$$$ e.conj(\mathrm{Id}) = \mathrm{Id} $$$

Lean4

/-- Given an `R`-module `M` and a function `m → n` between arbitrary types,
construct a linear map `(n → M) →ₗ[R] (m → M)` -/
def funLeft (f : m → n) : (n → M) →ₗ[R] m → M where
  toFun := (· ∘ f)
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

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