mul_one_div

Mathlib.Algebra.Group.Basic

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

English

In a division-monoid, x · (1/y) equals x/y for all x,y.

Русский

В моноиде с делением выполняется x · (1/y) = x/y для всех x,y.

LaTeX

$$$\forall x,y\in G,\ x \cdot (1/y) = x/y$$$

Lean4

@[to_additive]
theorem mul_one_div (x y : G) : x * (1 / y) = x / y := by rw [div_eq_mul_inv, one_mul, div_eq_mul_inv]

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

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

Разделы

Аффилиация

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