Sets as a semiring under union #
This file defines SetSemiring α
, an alias of Set α
, which we endow with ∪
as addition and
pointwise *
as multiplication. If α
is a (commutative) monoid, SetSemiring α
is a
(commutative) semiring.
An alias for Set α
, which has a semiring structure given by ∪
as "addition" and pointwise
multiplication *
as "multiplication".
Equations
Instances For
Equations
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
Equations
@[simp]
noncomputable instance
SetSemiring.instNonAssocSemiringOfMulOneClass
{α : Type u_1}
[MulOneClass α]
:
Equations
Equations
Equations
Equations
Equations
Equations
noncomputable def
SetSemiring.imageHom
{α : Type u_1}
{β : Type u_2}
[MulOneClass α]
[MulOneClass β]
(f : α →* β)
:
The image of a set under a multiplicative homomorphism is a ring homomorphism with respect to the pointwise operations on sets.
Equations
Instances For
theorem
SetSemiring.imageHom_def
{α : Type u_1}
{β : Type u_2}
[MulOneClass α]
[MulOneClass β]
(f : α →* β)
(s : SetSemiring α)
:
@[simp]
theorem
SetSemiring.down_imageHom
{α : Type u_1}
{β : Type u_2}
[MulOneClass α]
[MulOneClass β]
(f : α →* β)
(s : SetSemiring α)
:
@[simp]
theorem
Set.up_image
{α : Type u_1}
{β : Type u_2}
[MulOneClass α]
[MulOneClass β]
(f : α →* β)
(s : Set α)
: