Theorems · Definition · commutative algebra

MvPowerSeries.killCompl

{σ : Type u_1} →
  {τ : Type u_2} → {R : Type u_4} → [inst : CommSemiring R] → (σ ↪ τ) → MvPowerSeries τ R →ₐ[R] MvPowerSeries σ R

Given an embedding e : σ ↪ τ, MvPowerSeries.killComplFun e is the function from R⟦τ⟧ to R⟦σ⟧ that is left inverse to rename e.injective.fiberFinite : R⟦σ⟧ → R⟦τ⟧ and sends the variables in the complement of the range of e to 0.

Defined in

Mathlib.RingTheory.MvPowerSeries.Rename

Cited by

9 results in Mathlib

Foundations

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

Assumes

CommSemiring