instNontrivial

Mathlib.RingTheory.WittVector.Basic

URI: https://scilib.ai/kg/mathlib#WittVector.instNontrivial

English

If R is nontrivial, then the Witt vector ring 𝕎_p(R) is nontrivial as well.

Русский

Если R ненулевое, то и кольцо Witt 𝕎_p(R) тоже ненулево.

LaTeX

$$$$ \mathbb{W}_p(R) \neq \{0\} \quad\text{whenever } R \neq \{0\}. $$$$

Lean4

instance [Nontrivial R] : Nontrivial (𝕎 R) :=
  constantCoeff.domain_nontrivial

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru