Theorems · Theorem · commutative algebra

Subsemiring.center_toSubmonoid

∀ (R : Type u) [inst : NonAssocSemiring R],
  (Subsemiring.center R).toSubmonoid =
    { carrier := (NonUnitalSubsemiring.center R).carrier, mul_mem' := ⋯, one_mem' := ⋯ }

Defined in

Mathlib.Algebra.Ring.Subsemiring.Basic

Cited by

0 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NonAssocSemiring