English
The product of all elements m in finsetApprox(bS, adm) is nonzero under the algebra map from R to S; i.e. algebraMap_R_S(∏ m∈finsetApprox(bS adm), m) ≠ 0.
Русский
Произведение всех элементов m из finsetApprox(bS, adm) отображается в S ненулевым через алгебраическое отображение из R.
LaTeX
$$$ \\ algebraMap_R_S( \\prod_{m \\in \\mathrm{finsetApprox}(b_S, adm)} m ) \\neq 0 $$$
Lean4
/-- We can approximate `a / b : L` with `q / r`, where `r` has finitely many options for `L`. -/
theorem exists_mem_finset_approx' [Algebra.IsAlgebraic R S] (a : S) {b : S} (hb : b ≠ 0) :
∃ q : S, ∃ r ∈ finsetApprox bS adm, abv (Algebra.norm R (r • a - q * b)) < abv (Algebra.norm R b) :=
by
obtain ⟨a', b', hb', h⟩ := Algebra.IsAlgebraic.exists_smul_eq_mul R a hb
obtain ⟨q, r, hr, hqr⟩ := exists_mem_finsetApprox bS adm a' hb'
refine ⟨q, r, hr, ?_⟩
refine lt_of_mul_lt_mul_left ?_ (show 0 ≤ abv (Algebra.norm R (algebraMap R S b')) from abv.nonneg _)
refine
lt_of_le_of_lt (le_of_eq ?_)
(mul_lt_mul hqr le_rfl (abv.pos ((Algebra.norm_ne_zero_iff_of_basis bS).mpr hb)) (abv.nonneg _))
rw [← abv.map_mul, ← MonoidHom.map_mul, ← abv.map_mul, ← MonoidHom.map_mul, ← Algebra.smul_def, smul_sub b', sub_mul,
smul_comm, h, mul_comm b a', Algebra.smul_mul_assoc r a' b, Algebra.smul_mul_assoc b' q b]
