eq_mul_inv_iff_mul_eq

Mathlib.Algebra.Group.Basic

URI: https://scilib.ai/kg/mathlib#eq_mul_inv_iff_mul_eq

← MathLib Explorer

English

The equivalence a = b · c^{-1} ⇔ a · c = b holds.

Русский

Эквивалентность a = b · c^{-1} ⇔ a · c = b.

LaTeX

$$$ a = b \cdot c^{-1} \iff a \cdot c = b $$$

Lean4

@[to_additive]
theorem eq_mul_inv_iff_mul_eq : 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