map_ne_one_iff

Mathlib.Algebra.Group.Equiv.Defs

URI: https://scilib.ai/kg/mathlib#EmbeddingLike.map_ne_one_iff

English

For an embedding-like map f, f(x) ≠ 1 iff x ≠ 1.

Русский

Для вложения-образного отображения f: f(x) ≠ 1 эквив. x ≠ 1.

LaTeX

$$$f x \neq 1 \iff x \neq 1$$$

Lean4

@[to_additive]
theorem map_ne_one_iff {f : F} {x : M} : f x ≠ 1 ↔ x ≠ 1 :=
  map_eq_one_iff.not

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

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

Разделы

Аффилиация

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