Theorems · Definition · commutative algebra

LocalSubring.copy

{R : Type u_1} → [inst : CommRing R] → (S : LocalSubring R) → (s : Set R) → s = ↑S.toSubring → LocalSubring R

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

Defined in

Mathlib.RingTheory.LocalRing.LocalSubring

Cited by

0 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Quot.sound

Assumes

CommRing