single_eq_zero_iff

Mathlib.RingTheory.HahnSeries.Basic

URI: https://scilib.ai/kg/mathlib#HahnSeries.single_eq_zero_iff

English

The equality single a r = 0 holds if and only if r = 0.

Русский

Равенство single a r = 0 верно тогда и только тогда, когда r = 0.

LaTeX

$$single a r = 0 \iff r = 0$$

Lean4

@[simp]
theorem single_eq_zero_iff {a : Γ} {r : R} : single a r = 0 ↔ r = 0 :=
  map_eq_zero_iff _ <| single_injective a

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

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

Разделы

Аффилиация

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