map_eq_zero_iff

Mathlib.RingTheory.RingInvo

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

English

For any RingInvo R and x, f x = 0 implies x = 0, i.e., f is injective on R.

Русский

Для RingInvo R и любого x: f(x) = 0 ⇒ x = 0, то есть отображение инъективно.

LaTeX

$$$f\ x = 0 \iff x = 0$$$

Lean4

theorem map_eq_zero_iff (f : RingInvo R) {x : R} : f x = 0 ↔ x = 0 :=
  f.toRingEquiv.map_eq_zero_iff

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

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

Разделы

Аффилиация

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