Theorems · Theorem · commutative algebra

Subring.copy_toSubsemiring

∀ {R : Type u} [inst : NonAssocRing R] (S : Subring R) (s : Set R) (hs : s = ↑S),
  (S.copy s hs).toSubsemiring = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯ }

Defined in

Mathlib.Algebra.Ring.Subring.Defs

Cited by

0 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext

Assumes

NonAssocRing