isConj_iff_eq

Mathlib.Algebra.Group.Conj

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

← MathLib Explorer

English

In a commutative monoid, IsConj a b holds iff a = b.

Русский

В коммутативном моноиде IsConj a b эквивалентно a = b.

LaTeX

$$$IsConj(a,b) \\iff a = b$$$

Lean4

@[simp]
theorem isConj_iff_eq {α : Type*} [CommMonoid α] {a b : α} : IsConj a b ↔ a = b :=
  ⟨fun ⟨c, hc⟩ =>
    by
    rw [SemiconjBy, mul_comm, ← Units.mul_inv_eq_iff_eq_mul, mul_assoc, c.mul_inv, mul_one] at hc
    exact hc, fun h => by rw [h]⟩

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

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

Разделы

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

Аффилиация

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