coe_eq_zero_of_pos_iff — Mathlib

English

If p > 0 and x > 0 then (x : AddCircle p) = 0 iff ∃ n ∈ ℕ with x = n·p.

Русский

Если p > 0 и x > 0, то (x : AddCircle p) = 0 тогда и только тогда, когда ∃ n ∈ ℕ, x = n·p.

LaTeX

$$$$ (0 < p) \land (0 < x) \Rightarrow \left( (x : AddCircle\ p) = 0 \iff \exists n \in \mathbb{N}, \ n \cdot p = x \right) $$$$

Lean4

theorem coe_eq_zero_of_pos_iff (hp : 0 < p) {x : 𝕜} (hx : 0 < x) : (x : AddCircle p) = 0 ↔ ∃ n : ℕ, n • p = x :=
  by
  rw [coe_eq_zero_iff]
  constructor <;> rintro ⟨n, rfl⟩
  · replace hx : 0 < n := by
      contrapose! hx
      simpa only [← neg_nonneg, ← zsmul_neg, zsmul_neg'] using zsmul_nonneg hp.le (neg_nonneg.2 hx)
    exact ⟨n.toNat, by rw [← natCast_zsmul, Int.toNat_of_nonneg hx.le]⟩
  · exact ⟨(n : ℤ), by simp⟩

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