charP_iff

Mathlib.Algebra.CharP.Algebra

URI: https://scilib.ai/kg/mathlib#Algebra.charP_iff

English

For a field K and a nontrivial algebra L over K, CharP K p holds if and only if CharP L p holds.

Русский

Для поля K и не тривиальной алгебры L над K, CharP K p эквивалентно CharP L p.

LaTeX

$$$( \\text{charP}_\\text{iff} (K,L) )(p) : \\CharP(K,p) \\iff \\CharP(L,p)$$$

Lean4

protected theorem charP_iff (p : ℕ) : CharP K p ↔ CharP L p :=
  (algebraMap K L).charP_iff_charP p

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

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

Разделы

Аффилиация

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