-rw-r--r-- 1839 leangoppa-20230726/Goppadecoding/zero.lean raw
import Mathlib.Tactic

namespace Goppadecoding

section lemmas_zero

theorem eq_if_sub_zero {R: Type _} [Ring R] {a b: R}:
  a - b = 0 → a = b :=
by
  intro ab0
  calc
    a = a - 0 := by rw[sub_zero]
    _ = a - (a - b) := by rw[ab0]
    _ = b := by rw[sub_sub_self]

theorem zero_if_mul_left_zero {R: Type _} [Ring R] [IsLeftCancelMulZero R] {x y: R}:
  x ≠ 0 → x*y = 0 → y = 0 := by
    intro xnonzero xy0
    have xyx0: x*y = x*0 := by calc
      x*y = 0 := xy0
      _ = x*0 := Eq.symm (MulZeroClass.mul_zero x)
    exact mul_left_cancel₀ xnonzero xyx0

theorem zero_if_mul_right_zero {R: Type _} [Ring R] [IsRightCancelMulZero R] {x y: R}:
  y ≠ 0 → x*y = 0 → x = 0 := by
    intro ynonzero xy0
    have xy0y: x*y = 0*y := by calc
      x*y = 0 := xy0
      _ = 0*y := Eq.symm (MulZeroClass.zero_mul y)
    exact mul_right_cancel₀ ynonzero xy0y

theorem nonzero_if_mul_left_nonzero {k: Type _} [Field k] {x y: k}:
  x*y ≠ 0 → y ≠ 0 := by
    contrapose
    simp only[not_ne_iff]
    intro yzero
    rw[yzero]
    norm_num

theorem nonzero_if_mul_right_nonzero {k: Type _} [Field k] {x y: k}:
  x*y ≠ 0 → x ≠ 0 := by
    contrapose
    simp only[not_ne_iff]
    intro xzero
    rw[xzero]
    norm_num

theorem nonzero_if_mul_left_one {k: Type _} [Field k] {x y: k}:
  x*y = 1 → y ≠ 0 := by
    contrapose
    simp only[not_ne_iff]
    intro yzero
    rw[yzero]
    norm_num

theorem eq_one_if_mul_eq_self {R: Type _} [Semiring R] [IsDomain R] {a b: R}:
  a ≠ 0 → a*b = a → b = 1 := by
    intro anonzero
    apply (mul_eq_left₀ anonzero).mp

theorem gcd_ne_zero_iff {R: Type _} [EuclideanDomain R] [DecidableEq R] {a b: R}:
  EuclideanDomain.gcd a b ≠ 0 ↔ a ≠ 0 ∨ b ≠ 0 := by
    simp only [ne_eq, EuclideanDomain.gcd_eq_zero_iff, not_and]
    exact imp_iff_not_or

end lemmas_zero