mod_smul — Mathlib

English

For any a in A, H.div (a · f) = a · H.div f.

Русский

Для любого a ∈ A верно: H.div (a · f) = a · H.div f.

LaTeX

$$$ \\mathrm{div}(a \\cdot f) = a \\cdot \\mathrm{div}(f). $$$

Lean4

@[simp]
theorem mod_smul [IsAdicComplete I A] : H.mod (a • f) = a • H.mod f :=
  by
  have H1 := (H.isWeierstrassDivisionAt_div_mod f).smul a
  have H2 := H.isWeierstrassDivisionAt_div_mod (a • f)
  exact (H.eq_of_mul_add_eq_mul_add H2.degree_lt H1.degree_lt (H2.eq_mul_add.symm.trans H1.eq_mul_add)).2

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