preimage_mul_left_one'

Mathlib.Algebra.Group.Pointwise.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.preimage_mul_left_one'

← MathLib Explorer

English

In a group, preimage of {1} under x → a^{-1} x is the singleton {a}.

Русский

В группе предобраз {1} под отображением x → a^{-1} x есть единственный элемент {a}.

LaTeX

$$$\operatorname{preimage} \{1\} (a^{-1} \cdot \cdot) = \{a\}$$$

Lean4

@[to_additive]
theorem preimage_mul_left_one' : preimage 1 (a⁻¹ * ·) (mul_right_injective _).injOn = { a } := by
  rw [preimage_mul_left_one, inv_inv]

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

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

Разделы

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

Аффилиация

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