instNontrivialOfNonempty

Mathlib.GroupTheory.FreeAbelianGroup

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

English

If α is nonempty, then FreeAbelianGroup α is nontrivial.

Русский

Если α непуста, то FreeAbelianGroup α ненулева.

LaTeX

$$$[Nonempty\\ α] \\Rightarrow FreeAbelianGroup α\\;\\text{ is nontrivial}$$$

Lean4

instance [Nonempty α] : Nontrivial (FreeAbelianGroup α) where
  exists_pair_ne :=
    let ⟨x⟩ := ‹Nonempty α›;
    ⟨0, of x, zero_ne_of _⟩

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

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

Разделы

Аффилиация

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