English
For a subset s of P, IsFractional S(span_R s) holds iff there exists a ∈ S such that a·b is integral for every b ∈ s.
Русский
Для подмножества s ⊆ P условие IsFractional(S, span_R s) эквивалентно существованию a ∈ S такого, что a·b целое для каждого b ∈ s.
LaTeX
$$$ \\mathrm{IsFractional}\\ S\\ (\\mathrm{span}\\ R\\ s) \\iff \\exists a \\in S, \\forall b \\in P,\\ b \\in s \\Rightarrow \\mathrm{IsInteger}\\ R (a \\cdot b) $$$
Lean4
theorem isFractional_span_iff {s : Set P} : IsFractional S (span R s) ↔ ∃ a ∈ S, ∀ b : P, b ∈ s → IsInteger R (a • b) :=
⟨fun ⟨a, a_mem, h⟩ => ⟨a, a_mem, fun b hb => h b (subset_span hb)⟩, fun ⟨a, a_mem, h⟩ =>
⟨a, a_mem, fun _ hb =>
span_induction (hx := hb) h
(by
rw [smul_zero]
exact isInteger_zero)
(fun x y _ _ hx hy => by
rw [smul_add]
exact isInteger_add hx hy)
fun s x _ hx => by
rw [smul_comm]
exact isInteger_smul hx⟩⟩
