instCommRing

Mathlib.RingTheory.Perfection

URI: https://scilib.ai/kg/mathlib#PreTilt.instCommRing

English

If there exists n with coeff(...) ≠ 0, then coeff at Nat.find h plus any k is also ≠ 0.

Русский

Если существует n с coeff ≠ 0, то коэффициент на позицию Nat.find h + k тоже не равен нулю.

LaTeX

$$coeff(...)(Nat.find h + k) ≠ 0$$

Lean4

instance : CommRing (PreTilt O p) :=
  Perfection.commRing p _

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

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

Разделы

Аффилиация

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