of_gt'

Mathlib.Algebra.Order.Monoid.Canonical.Defs

URI: https://scilib.ai/kg/mathlib#NeZero.of_gt'

← MathLib Explorer

English

If y > 1 in a canonically ordered AddClass with One, then y ≠ 0.

Русский

Если y > 1 в канонически упорядоченном классе с единицей, то y ≠ 0.

LaTeX

$$1 < y \Rightarrow y \neq 0$$

Lean4

instance (priority := 10) of_gt' {M : Type*} [AddZeroClass M] [Preorder M] [CanonicallyOrderedAdd M] [One M] {y : M}
    [Fact (1 < y)] : NeZero y :=
  of_gt <| @Fact.out (1 < y) _

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

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

Разделы

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

Аффилиация

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