invOf_div

Mathlib.Algebra.GroupWithZero.Invertible

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

English

If a and b are invertible and a/b is invertible, then (a/b)^{-1} = b/a.

Русский

Если a, b обратимы и a/b обратимо, то (a/b)^{-1} = b/a.

LaTeX

$$$ (a/b)^{-1} = b/a \\\\text{ when } a,b \\\\text{ invertible and } a/b \\\\text{ invertible}$$$

Lean4

theorem invOf_div (a b : α) [Invertible a] [Invertible b] [Invertible (a / b)] : ⅟(a / b) = b / a :=
  invOf_eq_right_inv (by simp [← mul_div_assoc])

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

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

Разделы

Аффилиация

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