inv_div'

Mathlib.Algebra.Group.Basic

URI: https://scilib.ai/kg/mathlib#inv_div'

English

In a Division Commutative Monoid, the inverse of a quotient equals the quotient of inverses: (a / b)⁻¹ = a⁻¹ / b⁻¹.

Русский

В любом моноиде с делением коммутативным верно: (a / b)⁻¹ = a⁻¹ / b⁻¹.

LaTeX

$$$ (a / b)^{-1} = a^{-1} / b^{-1} $$$

Lean4

@[to_additive]
theorem inv_div' : (a / b)⁻¹ = a⁻¹ / b⁻¹ := by simp

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

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

Разделы

Аффилиация

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