pow_dvd_mul_untiltAux_sub_untiltAux_mul

English

For x, y in PreTilt(O, p) and m, p^m divides ((x · y).untiltAux m) − (x.untiltAux m)(y.untiltAux m).

Русский

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

LaTeX

$$$(p : O)^{m} \mid ((x \cdot y).untiltAux m) - (x.untiltAux m)(y.untiltAux m)$$$

Lean4

theorem pow_dvd_mul_untiltAux_sub_untiltAux_mul (x y : PreTilt O p) (m : ℕ) :
    (p : O) ^ m ∣ (x * y).untiltAux m - (x.untiltAux m) * (y.untiltAux m) := by
  cases m with
  | zero => simp [untiltAux]
  | succ m =>
    simp only [untiltAux, map_mul, ← mul_pow]
    refine dvd_sub_pow_of_dvd_sub ?_ m
    rw [← mem_span_singleton, ← Ideal.Quotient.eq]
    simp

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