instFunLikeSubtypeDualMemDualAnnihilator

English

There is a natural FunLike structure on the type W.dualAnnihilator, i.e., elements of W.dualAnnihilator can be treated as linear maps from M to the base ring in a way that is injective and respects function equality.

Русский

Существует естественная структура FunLike на множестве W.dualAnnihilator, то есть элементы W.dualAnnihilator можно рассматривать как линейные отображения из M в базовое кольцо так, чтобы различия отображений соответствовали различия функций.

LaTeX

$$Instance (W : Submodule R M) : FunLike (W.dualAnnihilator) M R$$

Lean4

instance (W : Submodule R M) : FunLike (W.dualAnnihilator) M R
    where
  coe φ := φ.val
  coe_injective' φ ψ
    h := by
    ext
    simp only [funext_iff] at h
    exact h _

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