eq_one_iff

Mathlib.Algebra.Group.Semiconj.Basic

URI: https://scilib.ai/kg/mathlib#SemiconjBy.eq_one_iff

English

Let a be in a group G and h a SemiconjBy relation between a, x, y. Then x = 1 iff y = 1.

Русский

Пусть a ∈ G и h: SemiconjBy a x y. Тогда x = 1 эквивалентно y = 1.

LaTeX

$$$$\forall a\in G,\; h:\ SemiconjBy\ a\ x\ y\Rightarrow (x=1 \iff y=1).$$$$

Lean4

@[to_additive]
theorem eq_one_iff (h : SemiconjBy a x y) : x = 1 ↔ y = 1 := by
  rw [← conj_eq_one_iff (a := a) (b := x), h.eq, mul_inv_cancel_right]

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

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

Разделы

Аффилиация

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