mk_eq_zero — Mathlib

English

Let Γ be a partially ordered set and R a ring with zero. For any function f: Γ → R whose support is well-founded, the Hahn series constructed from f via HahnSeries.mk with a witness h is zero if and only if f is the zero function.

Русский

Пусть Γ частично упорядочено, и R — кольцо с нулём. Для любой функции f: Γ → R, чья поддержка является достоинством по отношению к порядку Γ (IsPWO), ряд Ханна, построенный как HahnSeries.mk f h, равен нулю тогда и только тогда, когда f = 0.

LaTeX

$$$HahnSeries.mk(f,h)=0 \iff f=0$$$

Lean4

@[simp]
theorem mk_eq_zero (f : Γ → R) (h) : HahnSeries.mk f h = 0 ↔ f = 0 := by
  simp_rw [HahnSeries.ext_iff, funext_iff, coeff_zero, Pi.zero_apply]

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