English
If i ∈ b.support and t is such that t•P.root(i) lies in the root range, then t is either 1 or -1.
Русский
Если i ∈ поддержка b и t таков, что t•P.root(i) лежит в диапазоне корня, то t ∈ {1, -1}.
LaTeX
$$$t = 1 \quad \text{or} \quad t = -1$$$
Lean4
theorem eq_one_or_neg_one_of_mem_support_of_smul_mem [Finite ι] [NoZeroSMulDivisors ℤ M] [NoZeroSMulDivisors ℤ N]
(i : ι) (h : i ∈ b.support) (t : R) (ht : t • P.root i ∈ range P.root) : t = 1 ∨ t = -1 :=
by
obtain ⟨z, hz⟩ := b.eq_one_or_neg_one_of_mem_support_of_smul_mem_aux i h t ht
obtain ⟨s, hs⟩ := IsUnit.exists_left_inv <| isUnit_of_mul_eq_one_right _ t hz
replace ht : s • P.coroot i ∈ range P.coroot := by
obtain ⟨j, hj⟩ := ht
simpa only [coroot_eq_smul_coroot_iff.mpr hj, smul_smul, hs, one_smul] using mem_range_self j
obtain ⟨w, hw⟩ := b.flip.eq_one_or_neg_one_of_mem_support_of_smul_mem_aux i h s ht
have : (z : R) * w = 1 := by simpa [mul_mul_mul_comm _ t _ s, mul_comm t s, hs] using congr_arg₂ (· * ·) hz hw
suffices z = 1 ∨ z = -1 by
rcases this with rfl | rfl
· left; simpa using hz
· right; simpa [neg_eq_iff_eq_neg] using hz
norm_cast at this
rw [Int.mul_eq_one_iff_eq_one_or_neg_one] at this
tauto
