map_eq_zero_iff

Mathlib.Algebra.Module.LinearMap.Defs

URI: https://scilib.ai/kg/mathlib#LinearMap.map_eq_zero_iff

English

If f is injective, then f x = 0 implies x = 0 (and conversely), i.e., ker f = {0}.

Русский

Если отображение.Injective, тогда f x = 0 эквивалентно x = 0 (якорная нулевой образ).

LaTeX

$$$ f(x) = 0 \iff x = 0 \quad \text{если } f\text{ инъективно}$$$

Lean4

@[simp]
theorem map_eq_zero_iff (h : Function.Injective f) {x : M} : f x = 0 ↔ x = 0 :=
  _root_.map_eq_zero_iff f h

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

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

Разделы

Аффилиация

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