English
For any a ≠ 0 and any b, there exist a', b', c' with a' and b' coprime and c' a' = a, c' b' = b.
Русский
Для любого a ≠ 0 и любого b существуют a', b', c', причем a' и b' без общих факторов, и c' a' = a, c' b' = b.
LaTeX
$$$\forall a, a \neq 0, \forall b,\; \exists a',b',c', \mathrm{IsRelPrime}(a',b') \land c' a' = a \land c' b' = b.$$$
Lean4
/-- If `a ≠ 0, b` are elements of a unique factorization domain, then dividing
out their common factor `c'` gives `a'` and `b'` with no factors in common. -/
theorem exists_reduced_factors : ∀ a ≠ (0 : R), ∀ b, ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b :=
by
intro a
refine induction_on_prime a ?_ ?_ ?_
· intros
contradiction
· intro a a_unit _ b
use a, b, 1
constructor
· intro p p_dvd_a _
exact isUnit_of_dvd_unit p_dvd_a a_unit
· simp
· intro a p a_ne_zero p_prime ih_a pa_ne_zero b
by_cases h : p ∣ b
· rcases h with ⟨b, rfl⟩
obtain ⟨a', b', c', no_factor, ha', hb'⟩ := ih_a a_ne_zero b
refine ⟨a', b', p * c', @no_factor, ?_, ?_⟩
· rw [mul_assoc, ha']
· rw [mul_assoc, hb']
· obtain ⟨a', b', c', coprime, rfl, rfl⟩ := ih_a a_ne_zero b
refine ⟨p * a', b', c', ?_, mul_left_comm _ _ _, rfl⟩
intro q q_dvd_pa' q_dvd_b'
rcases p_prime.left_dvd_or_dvd_right_of_dvd_mul q_dvd_pa' with p_dvd_q | q_dvd_a'
· have : p ∣ c' * b' := dvd_mul_of_dvd_right (p_dvd_q.trans q_dvd_b') _
contradiction
exact coprime q_dvd_a' q_dvd_b'
