Theorems · Theorem · ring theory

NonUnitalStarSubsemiring.mk.injEq

∀ {R : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : Star R] (toNonUnitalSubsemiring : NonUnitalSubsemiring R)
  (star_mem' : ∀ {a : R}, a ∈ toNonUnitalSubsemiring.carrier → star a ∈ toNonUnitalSubsemiring.carrier)
  (toNonUnitalSubsemiring_1 : NonUnitalSubsemiring R)
  (star_mem'_1 : ∀ {a : R}, a ∈ toNonUnitalSubsemiring_1.carrier → star a ∈ toNonUnitalSubsemiring_1.carrier),
  ({ toNonUnitalSubsemiring := toNonUnitalSubsemiring, star_mem' := star_mem' } =
      { toNonUnitalSubsemiring := toNonUnitalSubsemiring_1, star_mem' := star_mem'_1 }) =
    (toNonUnitalSubsemiring = toNonUnitalSubsemiring_1)

Defined in

Mathlib.Algebra.Star.NonUnitalSubsemiring

Cited by

0 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext

Assumes

NonUnitalNonAssocSemiringStar