integers

Mathlib.RingTheory.Valuation.ValuationSubring

URI: https://scilib.ai/kg/mathlib#Valuation.valuationSubring.integers

English

Again, the integers sit inside the valuation subring for the valuation.

Русский

Ещё раз: целые числа лежат в valuationSubring оценки.

LaTeX

$$Z \subseteq v.valuationSubring$$

Lean4

theorem integers : v.Integers v.valuationSubring :=
  Valuation.integer.integers _

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

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

Разделы

Аффилиация

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