tropEquiv_symm_coe_fn

Mathlib.Algebra.Tropical.Basic

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

English

The inverse equivalence tropEquiv.symm coincides with untrop.

Русский

Обратная эквивалентность tropEquiv.symm совпадает с untrop.

LaTeX

$$$\\mathrm{tropEquiv.symm} : \\mathrm{Tropical}\\,R \\to R = \\mathrm{untrop}$$$

Lean4

@[simp]
theorem tropEquiv_symm_coe_fn : (tropEquiv.symm : Tropical R → R) = untrop :=
  rfl

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

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

Разделы

Аффилиация

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