English
nthHomSeq is multiplicative: nthHomSeq f_compat (r s) equals product of nthHomSeq f_compat r and 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_mul (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_mul, ← Int.cast_sub, ← padicNorm.dvd_iff_norm_le, ← ZMod.intCast_zmod_eq_zero_iff_dvd]
dsimp [nthHom]
simp only [ZMod.natCast_val, RingHom.map_mul, Int.cast_sub, ZMod.intCast_cast, Int.cast_mul]
rw [ZMod.cast_mul (show p ^ n ∣ p ^ j from pow_dvd_pow _ hj), sub_self]
