extendDomain_eq_one_iff

Mathlib.Algebra.Group.End

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.extendDomain_eq_one_iff

← MathLib Explorer

English

For any e and f, e.extendDomain f = 1 iff e = 1.

Русский

Для любого e и f верно: e.extendDomain f = 1 эквивалентно e = 1.

LaTeX

$$$e.extendDomain f = 1 \iff e = 1$$$

Lean4

@[simp]
theorem extendDomain_eq_one_iff {e : Perm α} {f : α ≃ Subtype p} : e.extendDomain f = 1 ↔ e = 1 :=
  (injective_iff_map_eq_one' (extendDomainHom f)).mp (extendDomainHom_injective f) e

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

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

Разделы

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

Аффилиация

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