English
For CharZero, NoZeroSmulDivisors on M, and reduced P, multiples n of a root avoid the root's range when n ≥ 2.
Русский
При CharZero, NoZeroSmulDivisors на M и редуцированном P, кратные n корню избегают образа корня при n ≥ 2.
LaTeX
$$$$ n \\cdot P.root i \\notin \\operatorname{range}(P.root) \\quad (\\text{for } n \\ge 2). $$$$
Lean4
theorem nsmul_notMem_range_root [CharZero R] [NoZeroSMulDivisors ℤ M] [P.IsReduced] {n : ℕ} [n.AtLeastTwo] {i : ι} :
n • P.root i ∉ range P.root :=
by
have : ¬LinearIndependent R ![n • P.root i, P.root i] := by
simpa only [LinearIndependent.pair_iff, not_forall] using ⟨1, -(n : R), by simp [Nat.cast_smul_eq_nsmul], by simp⟩
rintro ⟨j, hj⟩
replace this : j = i ∨ P.root j = -P.root i := by
simpa only [← hj, IsReduced.linearIndependent_iff, not_and_or, not_not] using this
rcases this with rfl | this
· replace hj : (1 : ℤ) • P.root j = (n : ℤ) • P.root j := by simpa
rw [(smul_left_injective ℤ <| P.ne_zero j).eq_iff, eq_comm] at hj
have : 2 ≤ n := Nat.AtLeastTwo.prop
cutsat
· rw [← one_smul ℤ (P.root i), ← neg_smul, hj] at this
replace this : (n : ℤ) • P.root i = -1 • P.root i := by simpa
rw [(smul_left_injective ℤ <| P.ne_zero i).eq_iff] at this
cutsat
