theorem Monotone.finset_sum {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Preorder ι] [AddCommMonoid M] [Preorder M] [AddLeftMono M] {s : Finset κ} {f : κ → ι → M} (hf : ∀ k ∈ s, Monotone (f k)) : Monotone fun (i : ι) => ∑ k ∈ s, f k i

A finite sum of monotone functions is monotone.

theorem Monotone.const_smul_of_nonneg {ι : Type u_1} {α : Type u_2} {M : Type u_3} [Preorder ι] [Preorder α] [Preorder M] [Zero α] [SMul α M] [PosSMulMono α M] {f : ι → M} (hf : Monotone f) {c : α} (hc : 0 ≤ c) : Monotone fun (i : ι) => c • f i

Scalar multiplication by a nonnegative element preserves monotonicity.

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] [IsDomain R] [IsTorsionFree R M] [h : Nontrivial M] : finrank R M ≠ 0