instNontrivialSubalgebra — Mathlib

English

If Γ and R are nontrivial, the subalgebra Subalgebra R (HahnSeries Γ R) is nontrivial.

Русский

Если Γ и R ненули, подсистема Subalgebra R (HahnSeries Γ R) ненулевая.

LaTeX

$$$ \text{Nontrivial}(\text{Subalgebra}_R(\mathrm{HahnSeries}(\Gamma, R))) $$$

Lean4

instance [Nontrivial Γ] [Nontrivial R] : Nontrivial (Subalgebra R (HahnSeries Γ R)) :=
  ⟨⟨⊥, ⊤, by
      rw [Ne, SetLike.ext_iff, not_forall]
      obtain ⟨a, ha⟩ := exists_ne (0 : Γ)
      refine ⟨single a 1, ?_⟩
      simp only [Algebra.mem_bot, not_exists, Set.mem_range, iff_true, Algebra.mem_top]
      intro x
      rw [HahnSeries.ext_iff, funext_iff, not_forall]
      refine ⟨a, ?_⟩
      rw [coeff_single_same, algebraMap_apply, C_apply, coeff_single_of_ne ha]
      exact zero_ne_one⟩⟩

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