eq_or_eq_inv_of_mabs_eq

Mathlib.Algebra.Order.Group.Unbundled.Abs

URI: https://scilib.ai/kg/mathlib#eq_or_eq_inv_of_mabs_eq

← MathLib Explorer

English

If |a|_m = b, then either a = b or a = b^{-1}.

Русский

Если |a|_м = b, то либо a = b, либо a = b^{-1}.

LaTeX

$$$|a|_m = b \Rightarrow a = b \lor a = b^{-1}$$$

Lean4

@[to_additive]
theorem eq_or_eq_inv_of_mabs_eq (h : |a|ₘ = b) : a = b ∨ a = b⁻¹ := by
  simpa only [← h, eq_comm (a := |a|ₘ), inv_eq_iff_eq_inv] using mabs_choice a

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

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

Разделы

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

Аффилиация

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