Commit 2024-07-15 20:56 cb0404f4

View on Github →

feat(Algebra/Star/NonUnitalSubsemiring): Add NonUnitalStarSubsemiring (#12938) Definitions and basic properties of non-unital star subsemirings

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Star/NonUnitalSubsemiring.lean

added def NonUnitalStarSubsemiring.center

added theorem NonUnitalStarSubsemiring.coe_copy

added theorem NonUnitalStarSubsemiring.copy_eq

added theorem NonUnitalStarSubsemiring.mem_carrier

added structure NonUnitalStarSubsemiring

added structure SubStarSemigroup

Created Mathlib/Algebra/Star/Subsemiring.lean

added def StarSubsemiring.center

added theorem StarSubsemiring.coe_copy

added theorem StarSubsemiring.coe_mk

added theorem StarSubsemiring.coe_toSubsemiring

added theorem StarSubsemiring.copy_eq

added theorem StarSubsemiring.ext

added theorem StarSubsemiring.mem_carrier

added theorem StarSubsemiring.mem_toSubsemiring

added theorem StarSubsemiring.toSubsemiring_inj

added theorem StarSubsemiring.toSubsemiring_injective

added theorem StarSubsemiring.toSubsemiring_le_iff

added structure StarSubsemiring

added def SubStarSemigroup.center