-rw-r--r-- 1045 leangoppa-20230726/Goppadecoding/dvd.lean raw
import Mathlib.RingTheory.Polynomial.Basic

namespace Goppadecoding

section lemmas_dvd

theorem nonzero_if_dvd_one {k: Type _} [Field k] {x: k}:
  x ∣ 1 → x ≠ 0 :=
by
  contrapose
  simp only[ne_eq,not_not]
  intro x0
  rw[x0,zero_dvd_iff]
  simp only[one_ne_zero,not_false_eq_true]

theorem dvd_if_dvd_mul_left {R : Type _} [CommSemiring R] {x y z: R} (coprime: IsCoprime x y) (dvd: x ∣ y*z):
  x ∣ z :=
by
  cases coprime with | intro a acond =>
    cases acond with | intro b bcond =>
      cases dvd with | intro q qcond =>
        have h: z = x*(a*z+b*q) := by calc
          z = 1*z := by ring
          _ = (a*x+b*y)*z := by rw[← bcond]
          _ = a*x*z+b*(y*z) := by ring
          _ = a*x*z+b*(x*q) := by rw[qcond]
          _ = x*(a*z+b*q) := by ring
        apply Dvd.intro (a*z+b*q)
        simp only [← h]

theorem dvd_if_dvd_mul_right {R : Type _} [CommSemiring R] {x y z: R} (coprime: IsCoprime x z) (dvd: x ∣ y*z):
  x ∣ y :=
by
  rw[mul_comm] at dvd
  apply dvd_if_dvd_mul_left coprime dvd

end lemmas_dvd