Leading signs and variations of lists

The first nonzero sign determines the change in sign variations when a nonzero entry is prepended to a list.

def List.firstSign {R : Type u_1} [Zero R] [LinearOrder R] (l : List R) : SignType

The sign of the first nonzero entry of a list, or 0 if every entry is zero.

Equations

• l.firstSign = (Option.map (⇑SignType.sign) (List.filter (fun (v : R) => decide (v ≠ 0)) l).head?).getD 0

@[simp]

theorem List.firstSign_nil {R : Type u_1} [Zero R] [LinearOrder R] : [].firstSign = 0

@[simp]

theorem List.firstSign_zero_cons {R : Type u_1} [Zero R] [LinearOrder R] (l : List R) : (0 :: l).firstSign = l.firstSign

@[simp]

theorem List.firstSign_cons_of_ne_zero {R : Type u_1} [Zero R] [LinearOrder R] {a : R} (l : List R) (ha : a ≠ 0) : (a :: l).firstSign = SignType.sign a

theorem List.signVariations_cons {R : Type u_1} [Zero R] [LinearOrder R] {a : R} (l : List R) : (a :: l).signVariations = (if SignType.sign a * l.firstSign = -1 then 1 else 0) + l.signVariations

Prepending an entry a adds one sign variation exactly when its sign is opposite the sign of the next surviving entry.