LeanPool.BrauerGroupNew.Mathlib.RingTheory.NonUnitalSubsemiring.Defs #
Imported Lean Pool material for
LeanPool.BrauerGroupNew.Mathlib.RingTheory.NonUnitalSubsemiring.Defs.
@[simp]
theorem
NonUnitalSubsemiring.carrier_eq_coe
{R : Type u_1}
[NonUnitalSemiring R]
(S : NonUnitalSubsemiring R)
: