instNonemptyOfNontrivial

Mathlib.Algebra.Order.Archimedean.Class

URI: https://scilib.ai/kg/mathlib#FiniteMulArchimedeanClass.instNonemptyOfNontrivial

← MathLib Explorer

English

If M is nontrivial, then FiniteMulArchimedeanClass M is nonempty.

Русский

Если M не тривиальна, то FiniteMulArchimedeanClass M непуст.

LaTeX

$$$\text{Nonempty }(FiniteMulArchimedeanClass M)$$$

Lean4

@[to_additive]
instance [Nontrivial M] : Nonempty (FiniteMulArchimedeanClass M) :=
  by
  obtain ⟨x, hx⟩ := exists_ne (1 : M)
  exact ⟨mk x hx, by simpa using hx⟩

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

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

Разделы

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

Аффилиация

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