embDomain_eq_zero — Mathlib

English

For f : α ↪ β and l : α →₀ M, embDomain f l = 0 if and only if l = 0. In particular embDomain f preserves the zero element.

Русский

Для f : α ↪ β и l : α →₀ M верно embDomain f l = 0 тогда и только тогда, когда l = 0. В частности embDomain f сохраняет ноль.

LaTeX

$$$\\forall {α β : Type*} {M : Type*} [Zero M] (f : Function.Embedding α β) (l : α →₀ M),\\ embDomain f l = 0 \\iff l = 0$$$

Lean4

@[simp]
theorem embDomain_eq_zero {f : α ↪ β} {l : α →₀ M} : embDomain f l = 0 ↔ l = 0 :=
  (embDomain_injective f).eq_iff' <| embDomain_zero f

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