sign_cases_of_C_mul_pow_nonneg — Mathlib

English

Let R be a linearly ordered ring with PosMulStrictMono. If for all natural numbers n we have a*b^n ≥ 0, then either a = 0 or (a > 0 and b ≥ 0).

Русский

Пусть R — линейно упорядочённое кольцо с PosMulStrictMono. Если для любого натурального n верно a·b^n ≥ 0, то либо a = 0, либо (a > 0 и b ≥ 0).

LaTeX

$$$\forall a,b\in R,\ (\forall n\in\mathbb{N},\ 0\le a\,b^n)\ \Rightarrow\ (a = 0\lor (0

Lean4

theorem sign_cases_of_C_mul_pow_nonneg [PosMulStrictMono R] (h : ∀ n, 0 ≤ a * b ^ n) : a = 0 ∨ 0 < a ∧ 0 ≤ b :=
  by
  have : 0 ≤ a := by simpa only [pow_zero, mul_one] using h 0
  refine this.eq_or_lt'.imp_right fun ha ↦ ⟨ha, nonneg_of_mul_nonneg_right ?_ ha⟩
  simpa only [pow_one] using h 1

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