coe_eq_zero_iff — Mathlib

English

An element x ∈ 𝕜 represents zero in AddCircle p precisely when x is an integral multiple of p: there exists n ∈ ℤ such that x = n·p.

Русский

Элемент x ∈ 𝕜 нулевой в AddCircle p тогда и только тогда, когда x является целочисленным кратным p: существует n ∈ ℤ such that x = n·p.

LaTeX

$$$$ (x : AddCircle\ p) = 0 \iff \exists n \in \mathbb{Z}, \ n \cdot p = x $$$$

Lean4

theorem coe_eq_zero_iff {x : 𝕜} : (x : AddCircle p) = 0 ↔ ∃ n : ℤ, n • p = x := by simp [AddSubgroup.mem_zmultiples_iff]

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