pow_mem_range_pow_of_coprime — Mathlib

English

Let m and n be coprime and a be an element of a group with zero. Then a^m belongs to the range of the map x ↦ x^n if and only if a belongs to that range.

Русский

Пусть m и n взаимно просты и а принадлежит группе с нулем. Тогда a^m принадлежит образу карты x ↦ x^n тогда и только тогда, когда a принадлежит этому образу.

LaTeX

$$$$\\forall (a)\\; (m\\perp n) \\Rightarrow \\bigl(a^m \\in \\mathrm{Range}(\\cdot^n) \\iff a \\in \\mathrm{Range}(\\cdot^n)\\bigr).$$$$

Lean4

theorem pow_mem_range_pow_of_coprime (hmn : m.Coprime n) (a : α) :
    a ^ m ∈ Set.range (· ^ n : α → α) ↔ a ∈ Set.range (· ^ n : α → α) := by simp [pow_eq_pow_iff_of_coprime hmn.symm];
  aesop

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