one_ne_of

Mathlib.RingTheory.FreeCommRing

URI: https://scilib.ai/kg/mathlib#FreeCommRing.one_ne_of

English

1 ≠ of x for all x; the image of any generator is not the unit.

Русский

1 не равно of(x) для любого x; образ генератора не равен единице.

LaTeX

$$$ 1 \\neq \\mathrm{of}(x) $$$

Lean4

@[simp]
theorem one_ne_of (x : α) : 1 ≠ of x :=
  FreeAbelianGroup.of_injective.ne <| Multiset.zero_ne_singleton _

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

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

Разделы

Аффилиация

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