fst_eq_zero_iff_eps_dvd — Mathlib

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⟩

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