Theorems · Definition · commutative algebra

Subsemiring.copy

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

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

Defined in

Mathlib.Algebra.Ring.Subsemiring.Defs

Cited by

5 results in Mathlib

Foundations

Depth 17 from the axioms · uses no axioms

Assumes

NonAssocSemiring