Rank invariance under linear equivalence

The dependency library proves that winnability is invariant under linear equivalence. This module lifts that statement through the universal tests in the definition of divisor rank.

theorem Utilities.rank_geq_of_linear_equiv (G : CFGraph) {D E : CFDiv G} (hDE : linearEquiv G D E) (k : ℤ) (hRank : rankGeq G D k) : rankGeq G E k

Every rank lower bound is preserved under linear equivalence.

theorem Utilities.rank_eq_of_linear_equiv (G : CFGraph) {D E : CFDiv G} (hDE : linearEquiv G D E) : rank G D = rank G E

Linearly equivalent divisors have equal rank.

theorem Utilities.rank_add_effective_ge (G : CFGraph) (D E : CFDiv G) (hEffective : effective E) (r : ℤ) (hRank : rank G D ≥ r) : rank G (D + E) ≥ r

Adding an effective divisor preserves every rank lower bound.

theorem Utilities.BNExists_mono_degree {G : CFGraph} {r d d' : ℤ} (hDegree : d ≤ d') (hExists : BNExists G r d) : BNExists G r d'

A Brill--Noether witness can be padded with effective chips to any larger exact degree without decreasing its target rank.