eval_ker

Mathlib.LinearAlgebra.Dual.Basis

URI: https://scilib.ai/kg/mathlib#Module.Basis.eval_ker

English

The kernel of the evaluation map Dual.eval R M is trivial; in other words, ker(Dual.eval R M) = ⊥.

Русский

Ядро отображения оценки Dual.eval R M тривиально; то есть ker(Dual.eval R M) = {0}.

LaTeX

$$$ \\ker(\\mathrm{Dual.eval} \\; R\\; M) = \\{0\\} $$$

Lean4

theorem eval_ker {ι : Type*} (b : Basis ι R M) : LinearMap.ker (Dual.eval R M) = ⊥ :=
  ker_eq_bot_of_injective (eval_injective b)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru