Mathlib Map

Theorems · Inductive type · commutative algebra

MvPowerSeries.HasSubst

{σ : Type u_1} → {τ : Type u_4} → {S : Type u_5} → [CommRing S] → (σ → MvPowerSeries τ S) → Prop

Families of power series which can be substituted

Defined in
Mathlib.RingTheory.MvPowerSeries.Substitution
Cited by
74 results in Mathlib
Foundations
Depth 19 from the axioms · uses propext
Assumes
CommRing
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

MvPowerSeries.substAlgHom · cited by 24MvPowerSeries.substAlgHomMvPowerSeries.substAlgHom_apply · cited by 21MvPowerSeries.substAlgHom…MvPowerSeries.coe_substAlgHom · cited by 15MvPowerSeries.coe_substAl…MvPowerSeries.coeff_subst · cited by 15MvPowerSeries.coeff_substPowerSeries.HasSubst.const · cited by 15HasSubst.constMvPowerSeries.HasSubst.hasEval · cited by 14HasSubst.hasEvalMvPowerSeries.HasSubst.X_pow · cited by 11HasSubst.X_powMvPowerSeries.subst_comp_subst_apply · cited by 10MvPowerSeries.subst_comp_…MvPowerSeries.hasSubst_of_constantCoeff_zero · cited by 8MvPowerSeries.hasSubst_of…MvPowerSeries.constantCoeff_subst_eq_zero · cited by 7MvPowerSeries.constantCoe…MvPowerSeries.coeff_subst_finite · cited by 6MvPowerSeries.coeff_subst…MvPowerSeries.substAlgHom_eq_aeval · cited by 6MvPowerSeries.substAlgHom…PowerSeries.hasSubst_iff · cited by 6PowerSeries.hasSubst_iffMvPowerSeries.HasSubst.const_coeff · cited by 5HasSubst.const_coeffMvPowerSeries.substAlgHom.congr_simp · cited by 5substAlgHom.congr_simpCommRing · cited by 17173CommRingMvPowerSeries · cited by 659MvPowerSeriesMvPowerSeries.HasSubstCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by78

Results whose statement or proof uses this declaration.