Mathlib Map

Theorems · Definition · commutative algebra

PowerSeries.HasEval

{S : Type u_2} → [CommRing S] → [TopologicalSpace S] → S → Prop

Points at which evaluation of power series is well behaved

Defined in
Mathlib.RingTheory.PowerSeries.Evaluation
Cited by
28 results in Mathlib
Foundations
Depth 22 from the axioms · uses propext, Quot.sound
Assumes
CommRingTopologicalSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

PowerSeries.aeval · cited by 11PowerSeries.aevalPowerSeries.hasEval · cited by 7PowerSeries.hasEvalPowerSeries.hasEval_iff · cited by 4PowerSeries.hasEval_iffPowerSeries.HasEval.map · cited by 3HasEval.mapPowerSeries.HasSubst.hasEval · cited by 3HasSubst.hasEvalPowerSeries.hasEvalIdeal · cited by 2PowerSeries.hasEvalIdealPowerSeries.hasSum_eval₂ · cited by 2PowerSeries.hasSum_eval₂PowerSeries.coe_aeval · cited by 2PowerSeries.coe_aevalPowerSeries.continuous_aeval · cited by 2PowerSeries.continuous_ae…PowerSeries.eval₂Hom · cited by 1PowerSeries.eval₂HomPowerSeries.eval₂_unique · cited by 1PowerSeries.eval₂_uniquePowerSeries.HasEval.X · cited by 1HasEval.XPowerSeries.HasEval.mul_left · cited by 1HasEval.mul_leftPowerSeries.HasEval.zero · cited by 1HasEval.zeroPowerSeries.hasSum_aeval · cited by 1PowerSeries.hasSum_aevalTopologicalSpace · cited by 24529TopologicalSpaceCommRing · cited by 17173CommRingIsTopologicallyNilpotent · cited by 22IsTopologicallyNilpotentPowerSeries.HasEvalCITED BYCITES

Cites3

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

Cited by31

Results whose statement or proof uses this declaration.