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 :

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

  • carrier : Set M
  • mul_mem' : ∀ {a b : M}, a self.carrierb self.carriera * b self.carrier
  • star_mem' : ∀ {a : M}, a self.carrierstar a self.carrier

    The carrier of a StarSubset is closed under the star operation.

Instances For
    theorem SubStarSemigroup.star_mem' {M : Type v} [Mul M] [Star M] (self : SubStarSemigroup M) {a : M} (_ha : a self.carrier) :
    star a self.carrier

    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
    • add_mem' : ∀ {a b : R}, a self.carrierb self.carriera + b self.carrier
    • zero_mem' : 0 self.carrier
    • mul_mem' : ∀ {a b : R}, a self.carrierb self.carriera * b self.carrier
    • star_mem' : ∀ {a : R}, a self.carrierstar a self.carrier

      The carrier of a NonUnitalStarSubsemiring is closed under the star operation.

    Instances For
      theorem NonUnitalStarSubsemiring.star_mem' {R : Type v} [NonUnitalNonAssocSemiring R] [Star R] (self : NonUnitalStarSubsemiring R) {a : R} (_ha : a self.carrier) :
      star a self.carrier

      The carrier of a NonUnitalStarSubsemiring is closed under the star operation.

      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
        @[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