Commit 2025-03-17 22:47 f4c058ea

View on Github →

feat(Mathlib.RingTheory.MvPowerSeries.Evaluation): evaluation of power series (#15019) Define the evaluation of (Mv)PowerSeries in complete hausdorff linear algebras

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/MvPolynomial/Equiv.lean

added theorem MvPolynomial.eval₂_const_pUnitAlgEquiv

added theorem MvPolynomial.eval₂_const_pUnitAlgEquiv_symm

added theorem MvPolynomial.eval₂_pUnitAlgEquiv

added theorem MvPolynomial.eval₂_pUnitAlgEquiv_symm

added theorem MvPolynomial.pUnitAlgEquiv_monomial

added theorem MvPolynomial.pUnitAlgEquiv_symm_monomial

Modified Mathlib/RingTheory/Ideal/Basic.lean

added theorem Ideal.prod_mem

Modified Mathlib/RingTheory/MvPowerSeries/Basic.lean

Created Mathlib/RingTheory/MvPowerSeries/Evaluation.lean

added theorem MvPolynomial.toMvPowerSeries_denseRange

added theorem MvPolynomial.toMvPowerSeries_isDenseInducing

added theorem MvPolynomial.toMvPowerSeries_isUniformInducing

added theorem MvPolynomial.toMvPowerSeries_uniformContinuous

added theorem MvPowerSeries.HasEval.add

added theorem MvPowerSeries.HasEval.map

added theorem MvPowerSeries.HasEval.mul_left

added theorem MvPowerSeries.HasEval.mul_right

added theorem MvPowerSeries.HasEval.zero

added structure MvPowerSeries.HasEval

added theorem MvPowerSeries.aeval_coe

added theorem MvPowerSeries.aeval_eq_sum

added theorem MvPowerSeries.aeval_unique

added theorem MvPowerSeries.coe_aeval

added theorem MvPowerSeries.coe_eval₂Hom

added theorem MvPowerSeries.comp_aeval

added theorem MvPowerSeries.comp_eval₂

added theorem MvPowerSeries.continuous_aeval

added theorem MvPowerSeries.continuous_eval₂

added theorem MvPowerSeries.eval₂Hom_eq_extend

added theorem MvPowerSeries.eval₂_C

added theorem MvPowerSeries.eval₂_X

added theorem MvPowerSeries.eval₂_coe

added theorem MvPowerSeries.eval₂_eq_tsum

added theorem MvPowerSeries.eval₂_unique

added def MvPowerSeries.hasEvalIdeal

added theorem MvPowerSeries.hasSum_aeval

added theorem MvPowerSeries.hasSum_eval₂

added theorem MvPowerSeries.mem_hasEvalIdeal_iff

added theorem MvPowerSeries.uniformContinuous_eval₂

Modified Mathlib/RingTheory/MvPowerSeries/LinearTopology.lean

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

added theorem MvPolynomial.toMvPowerSeries_pUnitAlgEquiv

added theorem Polynomial.pUnitAlgEquiv_symm_toPowerSeries

Created Mathlib/RingTheory/PowerSeries/Evaluation.lean

added theorem PowerSeries.aeval_coe

added theorem PowerSeries.aeval_eq_sum

added theorem PowerSeries.aeval_unique

added theorem PowerSeries.coe_aeval

added theorem PowerSeries.coe_eval₂Hom

added theorem PowerSeries.comp_aeval

added theorem PowerSeries.comp_eval₂

added theorem PowerSeries.continuous_aeval

added theorem PowerSeries.continuous_eval₂

added theorem PowerSeries.eval₂_C

added theorem PowerSeries.eval₂_X

added theorem PowerSeries.eval₂_coe

added theorem PowerSeries.eval₂_eq_tsum

added theorem PowerSeries.eval₂_unique

added theorem PowerSeries.hasEval

added theorem PowerSeries.hasEval_iff

added theorem PowerSeries.hasSum_aeval

added theorem PowerSeries.hasSum_eval₂

added theorem PowerSeries.isTopologicallyNilpotent_X

added theorem PowerSeries.uniformContinuous_eval₂

Modified Mathlib/Topology/Algebra/LinearTopology.lean

added theorem IsLinearTopology.hasBasis_right_ideal

Modified Mathlib/Topology/Algebra/TopologicallyNilpotent.lean

added theorem IsTopologicallyNilpotent.mem_topologicalNilradical_iff

added def topologicalNilradical