theorem Set.indicator_apply_apply {ι : Type u_1} {Ω : Type u_2} {M : Type u_3} [Zero M] (s : Set ι) (f : ι → Ω → M) (i : ι) (ω : Ω) : s.indicator f i ω = s.indicator (fun (j : ι) => f j ω) i

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