eq_inv_mul_iff_mul_eq

Mathlib.Algebra.Group.Basic

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

← MathLib Explorer

English

The equivalence a^{-1} · b = c ⇔ b = a · c, and related variants.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem eq_inv_mul_iff_mul_eq : a = b⁻¹ * c ↔ b * a = c :=
  ⟨fun h ↦ by rw [h, mul_inv_cancel_left], fun h ↦ by rw [← h, inv_mul_cancel_left]⟩

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

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

Разделы

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

Аффилиация

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