Theorems · Definition · ring theory

NonUnitalStarSubsemiring.mk.noConfusion

{R : Type v} →
  {inst : NonUnitalNonAssocSemiring R} →
    {inst_1 : Star R} →
      {P : Sort u} →
        {toNonUnitalSubsemiring : NonUnitalSubsemiring R} →
          {star_mem' : ∀ {a : R}, a ∈ toNonUnitalSubsemiring.carrier → star a ∈ toNonUnitalSubsemiring.carrier} →
            {toNonUnitalSubsemiring' : NonUnitalSubsemiring R} →
              {star_mem'' : ∀ {a : R}, a ∈ toNonUnitalSubsemiring'.carrier → star a ∈ toNonUnitalSubsemiring'.carrier} →
                { toNonUnitalSubsemiring := toNonUnitalSubsemiring, star_mem' := star_mem' } =
                    { toNonUnitalSubsemiring := toNonUnitalSubsemiring', star_mem' := star_mem'' } →
                  (toNonUnitalSubsemiring ≍ toNonUnitalSubsemiring' → P) → P

Defined in

Mathlib.Algebra.Star.NonUnitalSubsemiring

Cited by

1 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms