ne_zero_of_eq_add_single — Mathlib

English

If x = y + single x.order x.leadingCoeff and y ≠ 0, then x ≠ 0.

Русский

Если x = y + единичный член в порядке x и при этом y ≠ 0, то x ≠ 0.

LaTeX

$$$$ x \neq 0 \text{ given } x = y + \operatorname{single}(x.order)\, x.leadingCoeff \text{ and } y \neq 0. $$$$

Lean4

theorem ne_zero_of_eq_add_single [Zero Γ] {x y : HahnSeries Γ R} (hxy : x = y + single x.order x.leadingCoeff)
    (hy : y ≠ 0) : x ≠ 0 := by
  by_contra h
  simp only [h, order_zero, leadingCoeff_zero, map_zero, add_zero] at hxy
  exact hy hxy.symm

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