valuation

Mathlib.RingTheory.Valuation.ValuationSubring

URI: https://scilib.ai/kg/mathlib#ValuationSubring.valuation

English

Any valuation subring A of K induces a valuation on K with value group A.ValueGroup.

Русский

Любое оценочное подкольцо A в K задаёт оценку на K с группой значений A.ValueGroup.

LaTeX

$$$valuation: Valuation\;K\;A.ValueGroup$$$

Lean4

/-- Any valuation subring of `K` induces a natural valuation on `K`. -/
def valuation : Valuation K A.ValueGroup :=
  ValuationRing.valuation A K

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

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

Разделы

Аффилиация

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