Theorems · Definition · commutative algebra
MvPowerSeries.rename
{σ : Type u_1} →
{τ : Type u_2} →
{R : Type u_4} →
(f : σ → τ) → [Filter.TendstoCofinite f] → [inst : CommSemiring R] → MvPowerSeries σ R →ₐ[R] MvPowerSeries τ RRename all the variables in a multivariable power series by a map with finite fibers.
- Defined in
- Mathlib.RingTheory.MvPowerSeries.Rename
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommSemiringstatement and proof · cited by 10,911
- AlgHomstatement · cited by 3,236
- MvPowerSeriesstatement · cited by 659
- Filter.TendstoCofinitestatement and proof · cited by 28
- MvPowerSeries.renameFunproof · cited by 1
Cited by28
Results whose statement or proof uses this declaration.
- PowerSeries.toMvPowerSeriesproof · cited by 11
- MvPowerSeries.coeff_renamestatement and proof · cited by 7
- MvPowerSeries.renameEquivproof · cited by 4
- PowerSeries.toMvPowerSeries_applystatement · cited by 4
- MvPowerSeries.coeff_coeff_finSuccEquivproof · cited by 3
- MvPowerSeries.coeff_embDomain_renamestatement · cited by 3
- MvPowerSeries.rename_renamestatement and proof · cited by 3
- MvPowerSeries.renameEquiv_applystatement · cited by 2
- MvPowerSeries.rename_Cstatement · cited by 2
- MvPowerSeries.rename_Xstatement and proof · cited by 2
- MvPowerSeries.rename_eq_subststatement · cited by 2
- MvPowerSeries.rename_idstatement · cited by 2