units_inv_symm_left_iff

Mathlib.Algebra.Group.Semiconj.Units

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

← MathLib Explorer

English

For units a, SemiconjBy (a^{-1}) y x iff SemiconjBy a x y.

Русский

Для единиц a верно: SemiconjBy a^{-1} y x ⇔ SemiconjBy a x y.

LaTeX

$$$$\forall a\in M^{\times},\ x,y\in M:\ SemiconjBy a^{-1} y x \iff SemiconjBy a x y.$$$$

Lean4

@[to_additive (attr := simp)]
theorem units_inv_symm_left_iff {a : Mˣ} {x y : M} : SemiconjBy (↑a⁻¹) y x ↔ SemiconjBy (↑a) x y :=
  ⟨units_inv_symm_left, units_inv_symm_left⟩

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

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

Разделы

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

Аффилиация

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