Frobenius noncancellation from injectivity of finite coefficient jets. These are statements about power series in prime-power characteristic.

theorem CCDN.powerSeries_frobenius_relation_trivial {K : Type u_1} {ι : Type u_2} [Field K] [Fintype ι] (p r : ℕ) [Fact (Nat.Prime p)] [CharP K p] (f : ι → PowerSeries K) (hjet : ∀ (a : ι → K), (∀ n < p ^ r, (PowerSeries.coeff n) (∑ i : ι, a i • f i) = 0) → ∀ (i : ι), a i = 0) (g : ι → PowerSeries K) (hrel : ∑ i : ι, f i * g i ^ p ^ r = 0) (i : ι) : g i = 0

Independent jets of length p^r prevent any nontrivial relation with p^r-th-power power-series coefficients.