coe_eq_zero — Mathlib

English

For any element x in Icc(0,1), its image in the ambient ring is zero if and only if x is the zero element of the interval.

Русский

Для любого элемента x из Icc(0,1) его образ в кольце равен нулю тогда и только тогда, когда x является нулём интервала.

LaTeX

$$↑x = 0 \iff x = 0$$

Lean4

@[simp, norm_cast]
theorem coe_eq_zero {x : Icc (0 : R) 1} : (x : R) = 0 ↔ x = 0 :=
  by
  symm
  exact Subtype.ext_iff

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