tropEquiv_coe_fn

Mathlib.Algebra.Tropical.Basic

URI: https://scilib.ai/kg/mathlib#Tropical.tropEquiv_coe_fn

English

The function part of the equivalence tropEquiv coincides with the tropicalization map trop.

Русский

Функциональная часть эквивалентности tropEquiv совпадает с отображением trop.

LaTeX

$$$\\mathrm{tropEquiv} : R \\to \\mathrm{Tropical}\\,R$ satisfies $\\mathrm{tropEquiv} = \\mathrm{trop}$$$

Lean4

@[simp]
theorem tropEquiv_coe_fn : (tropEquiv : R → Tropical R) = trop :=
  rfl

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

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

Разделы

Аффилиация

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