val_symm_eq

Mathlib.Algebra.Order.Archimedean.Class

URI: https://scilib.ai/kg/mathlib#MulArchimedeanOrder.val_symm_eq

English

The val.symm equals the of.

Русский

val.symm равно of.

LaTeX

$$$$ (val (M := M)).symm = of. $$$$

Lean4

@[to_additive (attr := simp)]
theorem val_symm_eq : (val (M := M)).symm = of :=
  rfl

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

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

Разделы

Аффилиация

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