embed_mk

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

URI: https://scilib.ai/kg/mathlib#ValuativeRel.ValueGroupWithZero.embed_mk

English

For any γ in ValueGroupWithZero R, embed (valuation R) γ = γ.

Русский

Для любого γ в ValueGroupWithZero R отображение embed(valuation R)(γ) равно γ.

LaTeX

$$$\\mathrm{embed}(\\mathrm{valuation}\\;R)(\\gamma) = \\gamma$$$

Lean4

@[simp]
theorem embed_mk [v.Compatible] (x : R) (s : posSubmonoid R) : embed v (.mk x s) = v x / v (s : R) :=
  rfl

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

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

Разделы

Аффилиация

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