ext — Mathlib

English

Two HahnModule elements are equal if their images under the Of R equivalence have equal coefficients.

Русский

Два элемента HahnModule равны, если их образы через эквиверенцию Of R имеют одинаковые коэффициенты.

LaTeX

$$$x = y \Rightarrow ((\mathrm{of} \ R)^{-1} x).\mathrm{coeff} = ((\mathrm{of} \ R)^{-1} y).\mathrm{coeff}$$$

Lean4

@[ext]
theorem ext (x y : HahnModule Γ R V) (h : ((of R).symm x).coeff = ((of R).symm y).coeff) : x = y :=
  (of R).symm.injective <| HahnSeries.coeff_inj.1 h

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