pi'

Mathlib.Algebra.CharP.Pi

URI: https://scilib.ai/kg/mathlib#CharP.pi'

English

The same CharP property holds for Pi-spaces by a simple alias.

Русский

Та же характеристическая величина держится для Pi-пространств по простой альтернативе.

LaTeX

$$$\\text{CharP}\\; (\\iota \\to R) \\ p$$$

Lean4

instance pi' (ι : Type u) [Nonempty ι] (R : Type v) [CommRing R] (p : ℕ) [CharP R p] : CharP (ι → R) p :=
  CharP.pi ι R p

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

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

Разделы

Аффилиация

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