mabs_inv

Mathlib.Algebra.Order.Group.Unbundled.Abs

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

English

The modulus is invariant under taking inverses: |a^{-1}|_m = |a|_m.

Русский

Модуль не изменяется при взятии обратного: |a^{-1}|_м = |a|_м.

LaTeX

$$|a^{-1}|_m = |a|_m$$

Lean4

@[to_additive (attr := simp)]
theorem mabs_inv (a : α) : |a⁻¹|ₘ = |a|ₘ := by simp [mabs, sup_comm]

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

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

Разделы

Аффилиация

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