instNontrivialOfNonempty — Mathlib

English

If Γ is nonempty and R is nontrivial, then the Hahn series ring is nontrivial.

Русский

Если Γ непусто и R ненулевое, то кольцо ряда Ханна ненулевое.

LaTeX

$$Nontrivial (HahnSeries Γ R) for Nonempty Γ and Nontrivial R$$

Lean4

instance [Nonempty Γ] [Nontrivial R] : Nontrivial (HahnSeries Γ R) :=
  ⟨by
    obtain ⟨r, s, rs⟩ := exists_pair_ne R
    inhabit Γ
    refine ⟨single default r, single default s, fun con => rs ?_⟩
    rw [← coeff_single_same (default : Γ) r, con, coeff_single_same]⟩

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