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)
:
@[simp]
theorem
Nat.cast_finsetInf'
{ι : Type u_1}
{R : Type u_2}
[Semiring R]
[LinearOrder R]
[IsStrictOrderedRing R]
{s : Finset ι}
(f : ι → ℕ)
(hs : s.Nonempty)
:
@[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 : ι → ℕ)
:
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)
:
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)
:
Also see Finset.sup'_mul₀
for a version for GroupWithZero
s.