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

      The actual NonUnitalStarSubsemiring obtained from an element of a type satisfying NonUnitalSubsemiringClass and StarMemClass.

      Equations
      Instances For
        @[simp]
        @[instance 100]
        instance NonUnitalStarSubsemiring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallStar {R : Type v} [NonUnitalNonAssocSemiring R] [StarRing R] :
        CanLift (Set R) (NonUnitalStarSubsemiring R) SetLike.coe fun (s : Set R) => 0 s (∀ {x y : R}, x sy sx + y s) (∀ {x y : R}, x sy sx * y s) ∀ {x : R}, x sstar x s

        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
          @[simp]
          theorem NonUnitalStarSubsemiring.coe_copy {R : Type v} [NonUnitalNonAssocSemiring R] [StarRing R] (S : NonUnitalStarSubsemiring R) (s : Set R) (hs : s = S) :
          (S.copy s hs) = s
          theorem NonUnitalStarSubsemiring.copy_eq {R : Type v} [NonUnitalNonAssocSemiring R] [StarRing R] (S : NonUnitalStarSubsemiring R) (s : Set R) (hs : s = S) :
          S.copy s hs = S

          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