English
If p is prime and r ∈ ℚ with ⎯ ≤ 1, then p divides r.num − r.num · gcdA(r.den,p) mod p times r.den.
Русский
Если p простое и r ∈ ℚ с условием, что норма ≤ 1, то p делит r.num − r.num·gcdA(r.den,p) mod p умноженное на r.den.
LaTeX
$$$p \\\\mid r.\\\\num - r.\\\\num \\\\cdot r.\\\\den.gcdA(p) \\\\bmod p \\\\cdot r.den$$$
Lean4
theorem norm_sub_modPart_aux (r : ℚ) (h : ‖(r : ℚ_[p])‖ ≤ 1) : ↑p ∣ r.num - r.num * r.den.gcdA p % p * ↑r.den :=
by
rw [← ZMod.intCast_zmod_eq_zero_iff_dvd]
simp only [Int.cast_natCast, Int.cast_mul, Int.cast_sub]
have := congr_arg (fun x => x % p : ℤ → ZMod p) (gcd_eq_gcd_ab r.den p)
simp only [Int.cast_natCast, CharP.cast_eq_zero, EuclideanDomain.mod_zero, Int.cast_add, Int.cast_mul, zero_mul,
add_zero] at this
push_cast
rw [mul_right_comm, mul_assoc, ← this]
suffices rdcp : r.den.Coprime p by
rw [rdcp.gcd_eq_one]
simp only [mul_one, cast_one, sub_self]
apply Coprime.symm
apply (coprime_or_dvd_of_prime hp_prime.1 _).resolve_right
rw [← Int.natCast_dvd_natCast, ← norm_int_lt_one_iff_dvd, not_lt]
apply ge_of_eq
rw [← isUnit_iff]
exact isUnit_den r h
