-rw-r--r-- 1345 leangoppa-20230726/Goppadecoding/sq.lean raw
import Mathlib.RingTheory.Polynomial.Basic
import Mathlib.Algebra.Squarefree

open Polynomial

namespace Goppadecoding

section lemmas_sq

theorem mul_sq {R: Type _} [CommMonoid R] (a b: R):
  (a*b)^2 = a^2*b^2 := mul_pow a b 2

theorem div_sq {R: Type _} [DivisionCommMonoid R] (a b: R):
  (a/b)^2 = a^2/b^2 := div_pow a b 2

theorem div_sq_self_eq_recip {k: Type _} [Field k] (r: k): r / r^2 = 1 / r :=
by
  by_cases r0: r = 0
  . rw[r0,zero_pow,div_zero,div_zero]
    exact Nat.succ_pos 1
  have rrnonzero: r*r ≠ 0 := mul_ne_zero r0 r0
  apply eq_one_div_of_mul_eq_one_right
  rw[mul_div,sq]
  exact div_self rrnonzero

theorem div_sq_mul_mul {k: Type _} [Field k] (a b c: k): a / b^2 * (b*c) = a / b * c :=
by calc
  _ = a * c * (b / b^2) := by group
  _ = a * c * (1 / b) := by rw[div_sq_self_eq_recip b]
  _ = a / b * c := by group

theorem squarefree_dvd_square {k: Type _} [Field k] (g q: k[X]):
  Squarefree g → g ∣ q^2 → g ∣ q := by
    intro sqfree
    have twone0: 2 ≠ 0 := by norm_num
    exact (UniqueFactorizationMonoid.dvd_pow_iff_dvd_of_squarefree sqfree twone0).mp

theorem squarefree_dvd_square_2 {k: Type _} [Field k] (g q: k[X]):
  Squarefree g → g ∣ q^2 → g^2 ∣ q^2 := by
    intro sqfree gq2
    have gq: g ∣ q := squarefree_dvd_square g q sqfree gq2
    exact pow_dvd_pow_of_dvd gq 2

end lemmas_sq