eval_apply_eq_zero_iff

Mathlib.LinearAlgebra.Dual.Lemmas

URI: https://scilib.ai/kg/mathlib#Module.eval_apply_eq_zero_iff

English

For any v in V, ev_V(v) = 0 if and only if v = 0.

Русский

Для любого вектора v в V выполняется ev_V(v) = 0 тогда и только тогда, когда v = 0.

LaTeX

$$$(\\operatorname{ev}_V)(v) = 0 \\iff v = 0$$$

Lean4

theorem eval_apply_eq_zero_iff (v : V) : (eval K V) v = 0 ↔ v = 0 :=
  SetLike.ext_iff.mp (eval_ker K V) v

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

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

Разделы

Аффилиация

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