English
For any x ∈ K, there exist a ∈ A and b ∈ nonZeroDivisors A, with gcd(a,b)=1, such that the reduced fraction a/b represents x, i.e., IsLocalization.mk' K a b = x.
Русский
Для любого x ∈ K существует разложение x = a/b, где a ∈ A, b ∈ nonZeroDivisors A, gcd(a,b)=1 (IsRelPrime), и x равно выражению mk' K a b.
LaTeX
$$$\\exists a\\in A\\;\\exists b\\in \\text{nonZeroDivisors }A\\;\\big( \\mathrm{IsRelPrime}(a,b) \\land \\mathrm{IsLocalization.mk'} K a b = x \\big).$$$
Lean4
theorem exists_reduced_fraction (x : K) : ∃ (a : A) (b : nonZeroDivisors A), IsRelPrime a b ∧ mk' K a b = x :=
by
obtain ⟨⟨b, b_nonzero⟩, a, hab⟩ := exists_integer_multiple (nonZeroDivisors A) x
obtain ⟨a', b', c', no_factor, rfl, rfl⟩ :=
UniqueFactorizationMonoid.exists_reduced_factors' a b (mem_nonZeroDivisors_iff_ne_zero.mp b_nonzero)
obtain ⟨_, b'_nonzero⟩ := mul_mem_nonZeroDivisors.mp b_nonzero
refine ⟨a', ⟨b', b'_nonzero⟩, no_factor, ?_⟩
refine mul_left_cancel₀ (IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors b_nonzero) ?_
simp only [RingHom.map_mul, Algebra.smul_def] at *
rw [← hab, mul_assoc, mk'_spec' _ a' ⟨b', b'_nonzero⟩]
