mul_inv_eq_iff_eq_mul

Mathlib.Algebra.Group.Units.Basic

URI: https://scilib.ai/kg/mathlib#Units.mul_inv_eq_iff_eq_mul

← MathLib Explorer

English

For a,c in a monoid and b,d units, a b^{-1} = c ⇔ a = c b.

Русский

Для элементов a,c и единиц b,d в моноиде: a b^{-1} = c ⇔ a = c b.

LaTeX

$$$\forall a,c\in \alpha,\; \forall b,d\in \alpha^{\times}:\; a b^{-1} = c \iff a = c b$$$

Lean4

@[to_additive]
theorem mul_inv_eq_iff_eq_mul {a c : α} : a * ↑b⁻¹ = c ↔ a = c * b :=
  ⟨fun h => by rw [← h, inv_mul_cancel_right], fun h => by rw [h, mul_inv_cancel_right]⟩

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

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

Разделы

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

Аффилиация

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