of_map

Mathlib.Algebra.Group.Commute.Hom

URI: https://scilib.ai/kg/mathlib#Commute.of_map

← MathLib Explorer

English

If f is injective and f x and f y commute, then x and y commute.

Русский

Если f инъективно и f x и f y коммутируют, то x и y коммутируют.

LaTeX

$$$Function.Injective f \rightarrow Commute(f(x), f(y)) \Rightarrow Commute(x, y)$$$

Lean4

@[to_additive]
theorem of_map [MulHomClass F M N] {f : F} (hf : Function.Injective f) (h : Commute (f x) (f y)) : Commute x y :=
  hf (by simpa only [map_mul] using h.eq)

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

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

Разделы

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

Аффилиация

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