English
If σ is nonempty and R is nontrivial, then the subalgebra of MvPowerSeries σ R over R is nontrivial; in particular, there exist elements in Subalgebra R (MvPowerSeries σ R) that are beyond the bottom element.
Русский
Пусть множество σ непустое, а R несводимо; тогда подалгебра Subalgebra_R(MvPowerSeries_σ R) не тривиальна; существуют элементы, отличные от нуля, лежащие в этой подпалгебре.
LaTeX
$$$\\text{Nontrivial}(\\operatorname{Subalgebra}_R(\\mathrm{MvPowerSeries}_\\sigma R))$$$
Lean4
instance [Nonempty σ] [Nontrivial R] : Nontrivial (Subalgebra R (MvPowerSeries σ R)) :=
⟨⟨⊥, ⊤, by
classical
rw [Ne, SetLike.ext_iff, not_forall]
inhabit σ
refine ⟨X default, ?_⟩
simp only [Algebra.mem_bot, not_exists, Set.mem_range, iff_true, Algebra.mem_top]
intro x
rw [MvPowerSeries.ext_iff, not_forall]
refine ⟨Finsupp.single default 1, ?_⟩
simp [algebraMap_apply, coeff_C]⟩⟩
