of_ne_zero

Mathlib.GroupTheory.FreeAbelianGroup

URI: https://scilib.ai/kg/mathlib#FreeAbelianGroup.of_ne_zero

← MathLib Explorer

English

The image of generator is nonzero in FreeAbelianGroup α.

Русский

Образ генератора в FreeAbelianGroup α не равен 0.

LaTeX

$$$\\forall x:\\; of\\ x \\neq 0$$$

Lean4

@[simp]
theorem of_ne_zero (x : α) : of x ≠ 0 := by
  intro h
  let f : FreeAbelianGroup α →+ ℤ := lift 1
  have hfx : f (of x) = 1 := lift_apply_of _ _
  have hf0 : f (of x) = 0 := by rw [h, map_zero]
  exact one_ne_zero <| hfx.symm.trans hf0

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

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

Разделы

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

Аффилиация

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