Extra lemmas about canonically ordered monoids

@[simp]

theorem Finset.sup_eq_zero {ι : Type u_1} {α : Type u_2} [CanonicallyLinearOrderedAddCommMonoid α] {s : Finset ι} {f : ι → α} : s.sup f = 0 ↔ ∀ i ∈ s, f i = 0

@[simp]

theorem Finset.sup'_eq_zero {ι : Type u_1} {α : Type u_2} [CanonicallyLinearOrderedAddCommMonoid α] {s : Finset ι} {f : ι → α} (hs : s.Nonempty) : s.sup' hs f = 0 ↔ ∀ i ∈ s, f i = 0