zpow_y_lt_iff_lt — Mathlib

English

For a fundamental a, the relation (a^m).y < (a^n).y is equivalent to m < n.

Русский

Для фундаментального a отношение (a^m).y < (a^n).y эквивалентно m < n.

LaTeX

$$$\forall a\in \mathrm{Solution}_1(d),\; \text{IsFundamental}(a) \rightarrow \forall m,n\in \mathbb{Z},\; (a^m).y < (a^n).y \iff m < n$$$

Lean4

/-- If `a` is a fundamental solution, then `(a^m).y < (a^n).y` if and only if `m < n`. -/
theorem zpow_y_lt_iff_lt {a : Solution₁ d} (h : IsFundamental a) (m n : ℤ) : (a ^ m).y < (a ^ n).y ↔ m < n :=
  by
  refine ⟨fun H => ?_, fun H => h.y_strictMono H⟩
  contrapose! H
  exact h.y_strictMono.monotone H

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