English
For a prime p and i≥k, the p-adic powers satisfy a divisibility relation between aux g(p^{i}) and aux g(p^{k}) adjusted by cyclotomic structures.
Русский
Для простого p и i≥k выполняется отношение делимости между aux g(p^{i}) и aux g(p^{k}) с учётом циклотомической структуры.
LaTeX
$$$(p:\\mathbb{Z})^{k} \\mid \\operatorname{aux}g(p^{i}) - \\operatorname{aux}g(p^{k})$ при соответствующих условиях$$
Lean4
theorem pow_dvd_aux_pow_sub_aux_pow (g : L ≃+* L) (p : ℕ) [Fact p.Prime] [∀ i, HasEnoughRootsOfUnity L (p ^ i)]
{i k : ℕ} (hi : k ≤ i) : (p : ℤ) ^ k ∣ aux g (p ^ i) - aux g (p ^ k) :=
by
obtain ⟨i, rfl⟩ := exists_add_of_le hi
obtain ⟨ζ, hζ⟩ := HasEnoughRootsOfUnity.exists_primitiveRoot L (p ^ (k + i))
have h := hζ.pow (a := p ^ i) (Nat.pos_of_neZero _) (Nat.pow_add' _ _ _)
have h_unit : (h.isUnit NeZero.out).unit = (hζ.isUnit NeZero.out).unit ^ (p ^ i) := by ext; rfl
have H₁ := aux_spec g (p ^ (k + i)) ⟨_, (hζ.isUnit_unit NeZero.out).mem_rootsOfUnity⟩
have H₂ := aux_spec g (p ^ k) ⟨_, (h.isUnit_unit NeZero.out).mem_rootsOfUnity⟩
simp only [IsUnit.unit_spec, map_pow] at H₁ H₂
rw [H₁, ← Units.val_pow_eq_pow_val, ← Units.ext_iff, h_unit, ← div_eq_one] at H₂
simp only [← zpow_natCast, ← zpow_mul, div_eq_mul_inv, ← zpow_sub] at H₂
rw [(hζ.isUnit_unit NeZero.out).zpow_eq_one_iff_dvd, mul_comm, ← mul_sub] at H₂
conv_lhs at H₂ => rw [Nat.pow_add', Nat.cast_mul]
rwa [mul_dvd_mul_iff_left (by simp [NeZero.ne p]), Nat.cast_pow] at H₂
