Documentation

LeanPool.BrauerGroupNew.Mathlib.RingTheory.NonUnitalSubring.Defs

LeanPool.BrauerGroupNew.Mathlib.RingTheory.NonUnitalSubring.Defs #

Imported Lean Pool material for LeanPool.BrauerGroupNew.Mathlib.RingTheory.NonUnitalSubring.Defs.

source
@[simp]
theorem NonUnitalSubring.carrier_eq_coe {R : Type u_1} [NonUnitalRing R] (S : NonUnitalSubring R) :
S.carrier = ↑S