Documentation

Mathlib.Algebra.Order.Ring.Finset

Finset.sup and ring operations #

source
@[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)
source
@[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)
source
@[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)
source
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
source
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.