zpow_ne_neg_zpow — Mathlib

English

No power of a fundamental solution equals the negative of another power.

Русский

Ни одна степень фундаментального решения не равна отрицанию другой степени.

LaTeX

$$$\forall a\in \mathrm{Solution}_1(d), \text{IsFundamental}(a) \rightarrow \forall {n,n'\in \mathbb{Z}}, a^n \neq -a^{n'}$$$

Lean4

/-- A power of a fundamental solution is never equal to the negative of a power of this
fundamental solution. -/
theorem zpow_ne_neg_zpow {a : Solution₁ d} (h : IsFundamental a) {n n' : ℤ} : a ^ n ≠ -a ^ n' :=
  by
  intro hf
  apply_fun Solution₁.x at hf
  have H := x_zpow_pos h.x_pos n
  rw [hf, x_neg, lt_neg, neg_zero] at H
  exact lt_irrefl _ ((x_zpow_pos h.x_pos n').trans H)

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