instNontrivialSubalgebra — Mathlib

English

If R is nontrivial, then the subalgebra of power series R⟦X⟧ over R is nontrivial as an R-algebra.

Русский

Если R не тривиально, то подалгебра степенных рядов R⟦X⟧ над R не тривиальна.

LaTeX

$$$\\text{Nontrivial}(R) \\Rightarrow \\text{Nontrivial}(\\operatorname{Subalgebra} R (\\mathbb{R}[[X]]) )$$$

Lean4

instance [Nontrivial R] : Nontrivial (Subalgebra R R⟦X⟧) :=
  { inferInstanceAs <| Nontrivial <| Subalgebra R <| MvPowerSeries Unit R with }

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