op_div

Mathlib.Algebra.Group.Opposite

URI: https://scilib.ai/kg/mathlib#MulOpposite.op_div

English

For a DivInvMonoid α, op(x / y) = (op y)^{-1} * op x.

Русский

Для делимой группы α: op(x / y) = (op y)^{-1} * op x.

LaTeX

$$$ \mathrm{op\_div}(x,y):\; \mathrm{op}(x / y) = (\mathrm{op}\,y)^{-1} * \mathrm{op}\,x $$$

Lean4

@[to_additive (attr := simp)]
theorem op_div [DivInvMonoid α] (x y : α) : op (x / y) = (op y)⁻¹ * op x := by simp [div_eq_mul_inv]

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

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

Разделы

Аффилиация

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