Finset.sup and ring operations

@[simp]

theorem Nat.cast_finsetSup' {ι : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {s : Finset ι} (f : ι → ℕ) (hs : s.Nonempty) : ↑(s.sup' hs f) = s.sup' hs fun (i : ι) => ↑(f i)

@[simp]

theorem Nat.cast_finsetInf' {ι : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {s : Finset ι} (f : ι → ℕ) (hs : s.Nonempty) : ↑(s.inf' hs f) = s.inf' hs fun (i : ι) => ↑(f i)

@[simp]

theorem Nat.cast_finsetSup {ι : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [OrderBot R] [CanonicallyOrderedAdd R] (s : Finset ι) (f : ι → ℕ) : ↑(s.sup f) = s.sup fun (i : ι) => ↑(f i)

theorem Finset.mul_sup₀ {R : Type u_1} {ι : Type u_2} [LinearOrder R] [NonUnitalNonAssocSemiring R] [CanonicallyOrderedAdd R] [OrderBot R] (s : Finset ι) (f : ι → R) (a : R) : a * s.sup f = s.sup fun (x : ι) => a * f x

theorem Finset.sup_mul₀ {R : Type u_1} {ι : Type u_2} [LinearOrder R] [NonUnitalNonAssocSemiring R] [CanonicallyOrderedAdd R] [OrderBot R] (s : Finset ι) (f : ι → R) (a : R) : s.sup f * a = s.sup fun (x : ι) => f x * a

Also see Finset.sup'_mul₀ for a version for GroupWithZeros.