Finset.sup in a group

@[simp]

theorem Multiset.toFinset_nsmul {α : Type u_1} [DecidableEq α] (s : Multiset α) (n : ℕ) : n ≠ 0 → (n • s).toFinset = s.toFinset

theorem Multiset.toFinset_eq_singleton_iff {α : Type u_1} [DecidableEq α] (s : Multiset α) (a : α) : s.toFinset = {a} ↔ s.card ≠ 0 ∧ s = s.card • {a}

theorem Multiset.toFinset_card_eq_one_iff {α : Type u_1} [DecidableEq α] (s : Multiset α) : s.toFinset.card = 1 ↔ s.card ≠ 0 ∧ ∃ (a : α), s = s.card • {a}

theorem Finset.fold_max_add {ι : Type u_1} {M : Type u_3} [LinearOrder M] [Add M] [AddRightMono M] (s : Finset ι) (a : WithBot M) (f : ι → M) : fold max ⊥ (fun (i : ι) => ↑(f i) + a) s = fold max ⊥ (WithBot.some ∘ f) s + a

theorem Finset.inf'_pow {ι : Type u_1} {M : Type u_3} [LinearOrder M] [Monoid M] [MulLeftMono M] [MulRightMono M] (s : Finset ι) (f : ι → M) (n : ℕ) (hs : s.Nonempty) : s.inf' hs f ^ n = s.inf' hs fun (a : ι) => f a ^ n

theorem Finset.nsmul_inf' {ι : Type u_1} {M : Type u_3} [LinearOrder M] [AddMonoid M] [AddLeftMono M] [AddRightMono M] (s : Finset ι) (f : ι → M) (n : ℕ) (hs : s.Nonempty) : n • s.inf' hs f = s.inf' hs fun (a : ι) => n • f a

theorem Finset.sup'_pow {ι : Type u_1} {M : Type u_3} [LinearOrder M] [Monoid M] [MulLeftMono M] [MulRightMono M] (s : Finset ι) (f : ι → M) (n : ℕ) (hs : s.Nonempty) : s.sup' hs f ^ n = s.sup' hs fun (a : ι) => f a ^ n

theorem Finset.nsmul_sup' {ι : Type u_1} {M : Type u_3} [LinearOrder M] [AddMonoid M] [AddLeftMono M] [AddRightMono M] (s : Finset ι) (f : ι → M) (n : ℕ) (hs : s.Nonempty) : n • s.sup' hs f = s.sup' hs fun (a : ι) => n • f a

theorem Finset.sup'_mul {ι : Type u_1} {G : Type u_4} [Group G] [LinearOrder G] [MulRightMono G] (s : Finset ι) (f : ι → G) (a : G) (hs : s.Nonempty) : s.sup' hs f * a = s.sup' hs fun (i : ι) => f i * a

theorem Finset.sup'_add {ι : Type u_1} {G : Type u_4} [AddGroup G] [LinearOrder G] [AddRightMono G] (s : Finset ι) (f : ι → G) (a : G) (hs : s.Nonempty) : s.sup' hs f + a = s.sup' hs fun (i : ι) => f i + a

Also see Finset.sup'_add' that works for canonically ordered monoids.

theorem Finset.mul_sup' {ι : Type u_1} {G : Type u_4} [Group G] [LinearOrder G] [MulLeftMono G] (s : Finset ι) (f : ι → G) (a : G) (hs : s.Nonempty) : a * s.sup' hs f = s.sup' hs fun (i : ι) => a * f i

theorem Finset.add_sup' {ι : Type u_1} {G : Type u_4} [AddGroup G] [LinearOrder G] [AddLeftMono G] (s : Finset ι) (f : ι → G) (a : G) (hs : s.Nonempty) : a + s.sup' hs f = s.sup' hs fun (i : ι) => a + f i

Also see Finset.add_sup'' that works for canonically ordered monoids.

theorem Finset.sup'_add' {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [LinearOrder M] [CanonicallyOrderedAdd M] [Sub M] [AddLeftReflectLE M] [OrderedSub M] (s : Finset ι) (f : ι → M) (a : M) (hs : s.Nonempty) : s.sup' hs f + a = s.sup' hs fun (i : ι) => f i + a

Also see Finset.sup'_add that works for ordered groups.

theorem Finset.add_sup'' {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [LinearOrder M] [CanonicallyOrderedAdd M] [Sub M] [AddLeftReflectLE M] [OrderedSub M] {s : Finset ι} (hs : s.Nonempty) (f : ι → M) (a : M) : a + s.sup' hs f = s.sup' hs fun (i : ι) => a + f i

Also see Finset.add_sup' that works for ordered groups.

theorem Finset.sup_add {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [LinearOrder M] [CanonicallyOrderedAdd M] [Sub M] [AddLeftReflectLE M] [OrderedSub M] {s : Finset ι} [OrderBot M] (hs : s.Nonempty) (f : ι → M) (a : M) : s.sup f + a = s.sup fun (i : ι) => f i + a

theorem Finset.add_sup {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [LinearOrder M] [CanonicallyOrderedAdd M] [Sub M] [AddLeftReflectLE M] [OrderedSub M] {s : Finset ι} [OrderBot M] (hs : s.Nonempty) (f : ι → M) (a : M) : a + s.sup f = s.sup fun (i : ι) => a + f i

theorem Finset.sup_add_sup {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] [LinearOrder M] [CanonicallyOrderedAdd M] [Sub M] [AddLeftReflectLE M] [OrderedSub M] {s : Finset ι} {t : Finset κ} [OrderBot M] (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → M) (g : κ → M) : s.sup f + t.sup g = (s ×ˢ t).sup fun (ij : ι × κ) => f ij.1 + g ij.2