mul_div_cancel_right₀

Mathlib.Algebra.GroupWithZero.Defs

URI: https://scilib.ai/kg/mathlib#mul_div_cancel_right₀

English

In a MonoidWithZero with Div and MulDivCancelClass, for any a and any b ≠ 0, (a·b)/b = a.

Русский

В моноиде с нулём, в классе MulDivCancelClass выполняется: для любых a и ненулевого b: (a·b)/b = a.

LaTeX

$$$\forall a,b,\ b \neq 0 \Rightarrow (a \cdot b)/b = a$$$

Lean4

@[simp]
theorem mul_div_cancel_right₀ (a : M₀) {b : M₀} (hb : b ≠ 0) : a * b / b = a :=
  MulDivCancelClass.mul_div_cancel _ _ hb

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

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

Разделы

Аффилиация

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