ofPow — Mathlib

English

If Commute (↑u) a, then for any integer m, Commute (↑(u^m)) a.

Русский

Если Commute (↑u) a, то для любого целого m Commute (↑(u^m)) a.

LaTeX

$$Commute (↑u) a \Rightarrow ∀ m ∈ \mathbb{Z}, Commute (↑(u^m)) a$$

Lean4

/-- If a natural power of `x` is a unit, then `x` is a unit. -/
@[to_additive /-- If a natural multiple of `x` is an additive unit, then `x` is an additive unit. -/
    ]
def ofPow (u : Mˣ) (x : M) {n : ℕ} (hn : n ≠ 0) (hu : x ^ n = u) : Mˣ :=
  u.leftOfMul x (x ^ (n - 1))
    (by rwa [← _root_.pow_succ', Nat.sub_add_cancel (Nat.succ_le_of_lt <| Nat.pos_of_ne_zero hn)])
    (Commute.self_pow _ _)

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