Lean4
/-- Define `NormalizedGCDMonoid` on a structure just from the `lcm` and its properties. -/
noncomputable def normalizedGCDMonoidOfLCM [NormalizationMonoid α] [DecidableEq α] (lcm : α → α → α)
(dvd_lcm_left : ∀ a b, a ∣ lcm a b) (dvd_lcm_right : ∀ a b, b ∣ lcm a b)
(lcm_dvd : ∀ {a b c}, c ∣ a → b ∣ a → lcm c b ∣ a) (normalize_lcm : ∀ a b, normalize (lcm a b) = lcm a b) :
NormalizedGCDMonoid α :=
let exists_gcd a b := dvd_normalize_iff.2 (lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl))
{ (inferInstance : NormalizationMonoid α) with
lcm
gcd := fun a b => if a = 0 then normalize b else if b = 0 then normalize a else Classical.choose (exists_gcd a b)
gcd_mul_lcm := fun a b => by
split_ifs with h h_1
· rw [h, eq_zero_of_zero_dvd (dvd_lcm_left _ _), mul_zero, zero_mul]
· rw [h_1, eq_zero_of_zero_dvd (dvd_lcm_right _ _), mul_zero, mul_zero]
rw [mul_comm, ← Classical.choose_spec (exists_gcd a b)]
exact normalize_associated (a * b)
normalize_lcm
normalize_gcd := fun a b => by
dsimp [normalize]
split_ifs with h h_1
· apply normalize_idem
· apply normalize_idem
have h0 : lcm a b ≠ 0 := by
intro con
have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
rw [con, zero_dvd_iff, mul_eq_zero] at h
cases h
· exact absurd ‹a = 0› h
· exact absurd ‹b = 0› h_1
apply mul_left_cancel₀ h0
refine _root_.trans ?_ (Classical.choose_spec (exists_gcd a b))
conv_lhs =>
congr
rw [← normalize_lcm a b]
rw [← normalize_apply, ← normalize.map_mul, ← Classical.choose_spec (exists_gcd a b), normalize_idem]
lcm_zero_left := fun _ => eq_zero_of_zero_dvd (dvd_lcm_left _ _)
lcm_zero_right := fun _ => eq_zero_of_zero_dvd (dvd_lcm_right _ _)
gcd_dvd_left := fun a b => by
split_ifs with h h_1
· rw [h]
apply dvd_zero
· exact (normalize_associated _).dvd
have h0 : lcm a b ≠ 0 := by
intro con
have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
rw [con, zero_dvd_iff, mul_eq_zero] at h
cases h
· exact absurd ‹a = 0› h
· exact absurd ‹b = 0› h_1
rw [← mul_dvd_mul_iff_left h0, ← Classical.choose_spec (exists_gcd a b), normalize_dvd_iff, mul_comm,
mul_dvd_mul_iff_right h]
apply dvd_lcm_right
gcd_dvd_right := fun a b => by
split_ifs with h h_1
· exact (normalize_associated _).dvd
· rw [h_1]
apply dvd_zero
have h0 : lcm a b ≠ 0 := by
intro con
have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
rw [con, zero_dvd_iff, mul_eq_zero] at h
cases h
· exact absurd ‹a = 0› h
· exact absurd ‹b = 0› h_1
rw [← mul_dvd_mul_iff_left h0, ← Classical.choose_spec (exists_gcd a b), normalize_dvd_iff,
mul_dvd_mul_iff_right h_1]
apply dvd_lcm_left
dvd_gcd := fun {a b c} ac ab => by
split_ifs with h h_1
· apply dvd_normalize_iff.2 ab
· apply dvd_normalize_iff.2 ac
have h0 : lcm c b ≠ 0 := by
intro con
have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left c rfl)
rw [con, zero_dvd_iff, mul_eq_zero] at h
cases h
· exact absurd ‹c = 0› h
· exact absurd ‹b = 0› h_1
rw [← mul_dvd_mul_iff_left h0, ←
Classical.choose_spec (dvd_normalize_iff.2 (lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left c rfl))),
dvd_normalize_iff]
rcases ab with ⟨d, rfl⟩
rw [mul_eq_zero] at h_1
push_neg at h_1
rw [mul_comm a, ← mul_assoc, mul_dvd_mul_iff_right h_1.1]
apply lcm_dvd (Dvd.intro d rfl)
rw [mul_comm, mul_dvd_mul_iff_right h_1.2]
apply ac }
