coe_eq_zero_iff_of_mem_Ico — Mathlib

English

If a ∈ Ico 0 p, then (a : AddCircle p) = 0 iff a = 0.

Русский

Если a ∈ Ico 0 p, то (a : AddCircle p) = 0 тогда и только тогда, когда a = 0.

LaTeX

$$$$ (a : AddCircle\ p) = 0 \iff a = 0 \quad (a \in Ico\ 0\ p) $$$$

Lean4

theorem coe_eq_zero_iff_of_mem_Ico (ha : a ∈ Ico 0 p) : (a : AddCircle p) = 0 ↔ a = 0 :=
  by
  have h0 : 0 ∈ Ico 0 (0 + p) := by simpa [zero_add, left_mem_Ico] using hp.out
  have ha' : a ∈ Ico 0 (0 + p) := by rwa [zero_add]
  rw [← AddCircle.coe_eq_coe_iff_of_mem_Ico ha' h0, QuotientAddGroup.mk_zero]

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