English
nthHomSeq is additive: nthHomSeq f_compat (r+s) equals nthHomSeq f_compat r plus nthHomSeq f_compat s.
Русский
nthHomSeq сохраняет сложение: \nthHomSeq(f, r+s) = nthHomSeq(f,r) + nthHomSeq(f,s).
LaTeX
$$nthHomSeq f_compat (r+s) = nthHomSeq f_compat r + nthHomSeq f_compat s$$
Lean4
theorem nthHomSeq_add (r s : R) : nthHomSeq f_compat (r + s) ≈ nthHomSeq f_compat r + nthHomSeq f_compat s :=
by
intro ε hε
obtain ⟨n, hn⟩ := exists_pow_neg_lt_rat p hε
use n
intro j hj
dsimp [nthHomSeq]
apply lt_of_le_of_lt _ hn
rw [← Int.cast_add, ← Int.cast_sub, ← padicNorm.dvd_iff_norm_le, ← ZMod.intCast_zmod_eq_zero_iff_dvd]
dsimp [nthHom]
simp only [ZMod.natCast_val, RingHom.map_add, Int.cast_sub, ZMod.intCast_cast, Int.cast_add]
rw [ZMod.cast_add (show p ^ n ∣ p ^ j from pow_dvd_pow _ hj)]
simp only [sub_self]
