Theorems · Definition · commutative algebra

FreeCommRing.restriction

{α : Type u} → (s : Set α) → [DecidablePred fun x => x ∈ s] → FreeCommRing α →+* FreeCommRing ↑s

The restriction map from FreeCommRing α to FreeCommRing s where s : Set α, defined by sending all variables not in s to zero.

Defined in

Mathlib.RingTheory.FreeCommRing

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidablePred