map_ne_one_iff

Mathlib.Algebra.Group.Hom.Defs

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

← MathLib Explorer

English

If f is injective, then f x ≠ 1 implies x ≠ 1.

Русский

Если f инъективен, то f x ≠ 1 следовательно x ≠ 1.

LaTeX

$$$$ f x \neq 1 \Rightarrow x \neq 1. $$$$

Lean4

@[to_additive]
theorem map_ne_one_iff {R S F : Type*} [One R] [One S] [FunLike F R S] [OneHomClass F R S] (f : F)
    (hf : Function.Injective f) {x : R} : f x ≠ 1 ↔ x ≠ 1 :=
  (map_eq_one_iff f hf).not

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

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

Разделы

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

Аффилиация

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