instFaithfulSMulPolynomialLaurentSeries

English

The polynomial ring F[X] acts faithfully on Laurent series F⟨X⟩, i.e., if p·f = 0 for all f, then p = 0.

Русский

Поле F[X] действует достоверно на лорентовских разложениях F⟨X⟩: если p·f = 0 для всех f, то p = 0.

LaTeX

$$$\text{The action }\,F[X]\curvearrowright F⟨X⟩ \text{ is faithful.}$$$

Lean4

instance : FaithfulSMul F[X] F⸨X⸩ :=
  by
  refine (faithfulSMul_iff_algebraMap_injective F[X] F⸨X⸩).mpr ?_
  exact algebraMap_hahnSeries_injective ℤ

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