commute_map_iff

Mathlib.Algebra.Group.Commute.Hom

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

← MathLib Explorer

English

If f is injective, then Commute (f x) (f y) is equivalent to Commute x y.

Русский

Если f инъективно, то Commute(f x) (f y) эквивалентно Commute x y.

LaTeX

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

Lean4

@[to_additive]
theorem commute_map_iff [MulHomClass F M N] {f : F} (hf : Function.Injective f) {x y : M} :
    Commute (f x) (f y) ↔ Commute x y :=
  ⟨.of_map hf, (.map · f)⟩

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

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

Разделы

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

Аффилиация

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