lift_map_eq_zero_iff — Mathlib

English

The lifted map from R to A is zero if and only if the element of R is zero; i.e., the embedding is injective.

Русский

Поднятая карта из R в A равна нулю тогда и только тогда, когда элемент R равен нулю; т.е. вложение инъективно.

LaTeX

$$$ (↑a : A)=0 \\iff a=0 \\quad (a\\in R). $$$

Lean4

@[norm_cast]
theorem lift_map_eq_zero_iff (a : R) : (↑a : A) = 0 ↔ a = 0 :=
  map_eq_zero _

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