pow_eq_one_iff_of_nonneg

Stream: mathlib4

[Michael Stoll]

Do we really not have this?

import Mathlib.Algebra.GroupPower.Order

lemma pow_eq_one_iff_of_nonneg {R : Type*} [LinearOrderedRing R] {x : R} (hx : 0 ≤ x)
    {n : ℕ} (hn : n ≠ 0) : x ^ n = 1 ↔ x = 1 := by
  constructor
  · intro h
    exact le_antisymm ((pow_le_one_iff_of_nonneg hx hn).mp h.le)
      ((one_le_pow_iff_of_nonneg hx hn).mp h.ge)
  · rintro rfl
    exact one_pow _

[Yaël Dillies]

Nope. Missing. The lemmas around this are a real mess. I currently have a gitpod open fixing a few lemma names and it touches > 150 files.

[Michael Stoll]

Wold you like to include adding this to your future PR?

[Yaël Dillies]

Sure. I'll dump it in LeanCamCombi and it will get PRed in due course.

[Michael Stoll]

Since I needed it, I added that in #8449 .