theorem div_left_injective₀ {G₀ : Type u_1} [CommGroupWithZero G₀] {c : G₀} (hc : c ≠ 0) : Function.Injective fun (x : G₀) => x / c

@[simp]

theorem Module.finrank_ne_zero {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [StrongRankCondition R] [Module.Finite R M] [NoZeroSMulDivisors R M] [h : Nontrivial M] : finrank R M ≠ 0

theorem Fin.sum_Iic_sub {E : Type u_1} [AddCommGroup E] {n : ℕ} (a : Fin n) (f : Fin (n + 1) → E) : ∑ i ∈ Finset.Iic a, (f i.succ - f i.castSucc) = f a.succ - f 0

Telescopic sum when summing over Fin.