ringChar_eq

Mathlib.Algebra.CharP.Algebra

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

English

If K is a field and L is a nontrivial commutative L-algebra over K, then ringChar(K) = ringChar(L).

Русский

Если K — поле, а L не тривиально коммутативно-рациональная над K, тогда ringChar(K) = ringChar(L).

LaTeX

$$$\\text{ringChar}(K) = \\text{ringChar}(L)$$$

Lean4

theorem ringChar_eq : ringChar K = ringChar L :=
  by
  rw [ringChar.eq_iff, Algebra.charP_iff K L]
  apply ringChar.charP

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

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

Разделы

Аффилиация

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