embed_valuation

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

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

← MathLib Explorer

English

If v is compatible, then embed v is strictly monotone.

Русский

Если v совместима, тогда embed v строго монотонно.

LaTeX

$$$\\text{StrictMono}(\\mathrm{embed}(v))$$$

Lean4

@[simp]
theorem embed_valuation (γ : ValueGroupWithZero R) : embed (valuation R) γ = γ :=
  by
  induction γ using ValueGroupWithZero.ind
  simp [embed_mk, ← mk_eq_div]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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