Theorems · Definition · commutative algebra

Subring.copy

{R : Type u} → [inst : NonAssocRing R] → (S : Subring R) → (s : Set R) → s = ↑S → Subring R

Copy of a subring with a new carrier equal to the old one. Useful to fix definitional equalities.

Defined in

Mathlib.Algebra.Ring.Subring.Defs

Cited by

7 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext

Assumes

NonAssocRing