ne_one_of_map

Mathlib.Algebra.Group.Hom.Defs

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

← MathLib Explorer

English

If f x ≠ 1, then x ≠ 1 for a map f in a context with injectivity, ∀ x, f x ≠ 1 ⇒ x ≠ 1.

Русский

Если f x ≠ 1, то x ≠ 1 при инъективности отображения.

LaTeX

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

Lean4

@[to_additive]
theorem ne_one_of_map {R S F : Type*} [One R] [One S] [FunLike F R S] [OneHomClass F R S] {f : F} {x : R}
    (hx : f x ≠ 1) : x ≠ 1 :=
  ne_of_apply_ne f <| (by rwa [(map_one f)])

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

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

Разделы

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

Аффилиация

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