inv_mul_cancel_left₀

Mathlib.Algebra.GroupWithZero.Basic

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

← MathLib Explorer

English

In a CancelMonoidWithZero, if b ≠ 1 and b*a = a, then a = 0.

Русский

В CancelMonoidWithZero, если b ≠ 1 и b·a = a, то a = 0.

LaTeX

$$$$ b \neq 1 \land b \cdot a = a \Rightarrow a = 0 $$$$

Lean4

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

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

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

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

Разделы

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

Аффилиация

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