English
If i ∈ b.support and t is such that t•P.root(i) lies in the range of roots, then there exists an integer z with z·t = 1.
Русский
Пусть i принадлежит поддержке b и есть t such that t•P.root(i) лежит в диапазоне корней; тогда существует целое z, такое что z·t = 1.
LaTeX
$$$\exists z ∈ \mathbb{Z}, z \cdot t = 1$$$
Lean4
theorem eq_one_or_neg_one_of_mem_support_of_smul_mem_aux [Finite ι] [NoZeroSMulDivisors ℤ M] [NoZeroSMulDivisors ℤ N]
(i : ι) (h : i ∈ b.support) (t : R) (ht : t • P.root i ∈ range P.root) : ∃ z : ℤ, z * t = 1 := by
classical
obtain ⟨j, hj⟩ := ht
obtain ⟨f, hf⟩ : ∃ f : b.support → ℤ, P.coroot i = ∑ i, (t * f i) • P.coroot i :=
by
have : P.coroot j ∈ span ℤ (P.coroot '' b.support) := b.coroot_mem_span_int j
rw [image_eq_range, mem_span_range_iff_exists_fun] at this
refine this.imp fun f hf ↦ ?_
simp only [Finset.coe_sort_coe] at hf
simp_rw [mul_smul, ← Finset.smul_sum, Int.cast_smul_eq_zsmul, hf, coroot_eq_smul_coroot_iff.mpr hj]
use f ⟨i, h⟩
replace hf :
P.coroot i =
linearCombination R (fun k : b.support ↦ P.coroot k)
(t • (linearEquivFunOnFinite R _ _).symm (fun x ↦ (f x : R))) :=
by
rw [map_smul, linearCombination_eq_fintype_linearCombination_apply, Fintype.linearCombination_apply, hf]
simp_rw [mul_smul, ← Finset.smul_sum]
let g : b.support →₀ R := single ⟨i, h⟩ 1
have hg : P.coroot i = linearCombination R (fun k : b.support ↦ P.coroot k) g := by simp [g]
rw [hg] at hf
have : Injective (linearCombination R fun k : b.support ↦ P.coroot k) := b.linearIndepOn_coroot
simpa [g, linearEquivFunOnFinite, mul_comm t] using (DFunLike.congr_fun (this hf) ⟨i, h⟩).symm
