instCharZero_1

Mathlib.NumberTheory.NumberField.Basic

URI: https://scilib.ai/kg/mathlib#NumberField.RingOfIntegers.instCharZero_1

English

If K has characteristic zero, then 𝓞_K also has characteristic zero.

Русский

Если характеристика K равна нулю, то характеристика 𝓞_K равна нулю.

LaTeX

$$$\\operatorname{char}(\\mathcal{O}_K) = 0 \\quad\\text{whenever}\\quad \\operatorname{char}(K) = 0$$$

Lean4

instance [CharZero K] : CharZero (𝓞 K) :=
  CharZero.of_module _ K

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

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

Разделы

Аффилиация

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