Documentation

Mathlib.Algebra.Group.Pointwise.Set.Small

Small instances for pointwise operations #

instance small_set_zero {α : Type u_1} [Zero α] :
instance small_set_one {α : Type u_1} [One α] :
instance small_neg {α : Type u_1} (s : Set α) [InvolutiveNeg α] [Small.{u, u_1} s] :
instance small_add {α : Type u_1} (s t : Set α) [Add α] [Small.{u, u_1} s] [Small.{u, u_1} t] :
Small.{u, u_1} ↑(s + t)
instance small_sub {α : Type u_1} (s t : Set α) [Sub α] [Small.{u, u_1} s] [Small.{u, u_1} t] :
Small.{u, u_1} ↑(s - t)
instance small_mul {α : Type u_1} (s t : Set α) [Mul α] [Small.{u, u_1} s] [Small.{u, u_1} t] :
Small.{u, u_1} ↑(s * t)
instance small_div {α : Type u_1} (s t : Set α) [Div α] [Small.{u, u_1} s] [Small.{u, u_1} t] :
Small.{u, u_1} ↑(s / t)