pos

Mathlib.Algebra.Order.Ring.Canonical

URI: https://scilib.ai/kg/mathlib#Odd.pos

English

If a is odd in a canonically ordered additive structure, then a > 0.

Русский

Если a является нечетным элементом в канонически упорядоченной аддитивной структуре, то a > 0.

LaTeX

$$Theorem with 0 < a for Odd a$$

Lean4

theorem pos [Semiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [Nontrivial R] {a : R} : Odd a → 0 < a := by
  rintro ⟨k, rfl⟩; simp

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

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

Разделы

Аффилиация

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