inv_mul_cancel_right₀

Mathlib.Algebra.GroupWithZero.Basic

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

← MathLib Explorer

English

For GroupWithZero, if b ≠ 0, then a * b⁻¹ * b = a for all a.

Русский

Для GroupWithZero, если b ≠ 0, то ∀a: a b⁻¹ b = a.

LaTeX

$$$$ b \neq 0 \Rightarrow a \cdot b^{-1} \cdot b = a $$$$

Lean4

@[simp high] -- should take priority over `IsUnit.mul_inv_cancel_right`

theorem inv_mul_cancel_right₀ (h : b ≠ 0) (a : G₀) : a * b⁻¹ * b = a :=
  calc
    a * b⁻¹ * b = a * (b⁻¹ * b) := mul_assoc _ _ _
    _ = a := by simp [h]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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