pow_dvd_one_untiltAux_sub_one — Mathlib

English

For x = 1 in PreTilt(O, p), and any m, p^m divides untiltAux m − 1.

Русский

Для x = 1 в PreTilt(O, p) и любого m, p^m делит untiltAux m − 1.

LaTeX

$$$(p : O)^{m} \mid (1 : PreTilt O p).untiltAux m - 1$$$

Lean4

theorem pow_dvd_one_untiltAux_sub_one (m : ℕ) : (p : O) ^ m ∣ (1 : PreTilt O p).untiltAux m - 1 := by
  cases m with
  | zero => simp [untiltAux]
  | succ m =>
    simp only [untiltAux]
    nth_rw 3 [← one_pow (p ^ m)]
    refine dvd_sub_pow_of_dvd_sub (R := O) ?_ m
    rw [← mem_span_singleton, ← Ideal.Quotient.eq]
    simp

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