English
In the dual-number context, the first component is zero iff the epsilon element divides the whole element.
Русский
В контексте двойного числа первый компонент равен нулю тогда и только тогда, когда eps делит всё число.
LaTeX
$$$x.fst = 0 \Leftrightarrow \\varepsilon \\mid x$$$
Lean4
theorem fst_eq_zero_iff_eps_dvd [Semiring R] {x : R[ε]} : x.fst = 0 ↔ ε ∣ x :=
by
simp_rw [dvd_def, TrivSqZeroExt.ext_iff, TrivSqZeroExt.fst_mul, TrivSqZeroExt.snd_mul, fst_eps, snd_eps, zero_mul,
zero_smul, zero_add, MulOpposite.smul_eq_mul_unop, MulOpposite.unop_op, one_mul, exists_and_left, iff_self_and]
intro
exact ⟨.inl x.snd, rfl⟩