div

Mathlib.Algebra.Group.Units.Defs

URI: https://scilib.ai/kg/mathlib#IsUnit.div

English

For any α in a DivisionMonoid and unit b, b/(a·b) = a^{-1}.

Русский

Для любого α в делимом моноиде и единицы b: b/(a·b) = a^{-1}.

LaTeX

$$$\forall {\alpha} [DivisionMonoid\ \alpha] {b : \alpha}, IsUnit b \rightarrow \forall (a : \alpha), b/(a\cdot b) = a^{-1}$$$

Lean4

@[to_additive]
theorem div (ha : IsUnit a) (hb : IsUnit b) : IsUnit (a / b) := by rw [div_eq_mul_inv]; exact ha.mul hb.inv

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

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

Разделы

Аффилиация

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