Non-unital Star Subsemirings #
In this file we define NonUnitalStarSubsemiring
s and the usual operations on them.
Implementation #
This file is heavily inspired by Mathlib.Algebra.Star.NonUnitalSubalgebra
.
A sub star semigroup is a subset of a magma which is closed under the star
- carrier : Set M
The
carrier
of aStarSubset
is closed under thestar
operation.
Instances For
The carrier
of a StarSubset
is closed under the star
operation.
A non-unital star subsemiring is a non-unital subsemiring which also is closed under the
star
operation.
- carrier : Set R
- zero_mem' : 0 ∈ self.carrier
The
carrier
of aNonUnitalStarSubsemiring
is closed under thestar
operation.
Instances For
The carrier
of a NonUnitalStarSubsemiring
is closed under the star
operation.
Equations
- NonUnitalStarSubsemiring.instSetLike = { coe := fun {s : NonUnitalStarSubsemiring R} => s.carrier, coe_injective' := ⋯ }
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Copy of a non-unital star subsemiring with a new carrier
equal to the old one.
Useful to fix definitional equalities.
Equations
- S.copy s hs = { toNonUnitalSubsemiring := S.copy s hs, star_mem' := ⋯ }
Instances For
The center of a non-unital non-associative semiring R
is the set of elements that
commute and associate with everything in R
, here realized as non-unital star
subsemiring.
Equations
- NonUnitalStarSubsemiring.center R = { toNonUnitalSubsemiring := NonUnitalSubsemiring.center R, star_mem' := ⋯ }