Documentation

Mathlib.Algebra.Star.NonUnitalSubsemiring

Non-unital Star Subsemirings #

In this file we define NonUnitalStarSubsemirings and the usual operations on them.

Implementation #

This file is heavily inspired by Mathlib.Algebra.Star.NonUnitalSubalgebra.

structure SubStarSemigroup (M : Type v) [Mul M] [Star M] extends Subsemigroup M :

A sub star semigroup is a subset of a magma which is closed under the star

Instances For

    A non-unital star subsemiring is a non-unital subsemiring which also is closed under the star operation.

    Instances For

      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
        Instances For