mabs_eq

Mathlib.Algebra.Order.Group.Abs

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

← MathLib Explorer

English

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

Русский

Пусть b ≥ 1. Тогда |a|_м = b эквивалентно a = b или a = b^{-1}.

LaTeX

$$$\text{If } b \ge 1:\; |a|_m = b \iff a = b \lor a = b^{-1}$$$

Lean4

@[to_additive]
theorem mabs_eq (hb : 1 ≤ b) : |a|ₘ = b ↔ a = b ∨ a = b⁻¹ :=
  by
  refine ⟨eq_or_eq_inv_of_mabs_eq, ?_⟩
  rintro (rfl | rfl) <;> simp only [mabs_inv, mabs_of_one_le hb]

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

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

Разделы

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

Аффилиация

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