instExpChar — Mathlib

English

If R has exponent p in ExpChar, then the polynomial ring R[X] has ExpChar p as well.

Русский

Если у кольца R задано экспонентное характерное p, то и полиномиальная кольцо R[X] имеет ExpChar p.

LaTeX

$$$ \\forall (p : \\mathbb{N}) [h : \\mathrm{ExpChar} \\, R \\, p], \\; \\mathrm{ExpChar} (\\mathbb{R}[X]) p. $$$

Lean4

instance instExpChar (p : ℕ) [h : ExpChar R p] : ExpChar R[X] p := by cases h; exacts [ExpChar.zero, ExpChar.prime ‹_›]

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