abs_one_div

Mathlib.Algebra.Order.Field.Basic

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

English

|1 / a| = 1 / |a|.

Русский

|1 / a| = 1 / |a|.

LaTeX

$$|1 / a| = 1 / |a|$$

Lean4

theorem abs_one_div (a : α) : |1 / a| = 1 / |a| := by rw [abs_div, abs_one]

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

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

Разделы

Аффилиация

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