Documentation Verification Report

HEval

📁 Source: Mathlib/RingTheory/HahnSeries/HEval.lean

Statistics

Metric	Count
Definitions `powerSeriesFamily`, `heval`	2
Theorems `hsum_powerSeriesFamily_mul`, `powerSeriesFamily_add`, `powerSeriesFamily_hsum_zero`, `powerSeriesFamily_of_not_orderTop_pos`, `powerSeriesFamily_of_orderTop_pos`, `powerSeriesFamily_smul`, `support_powerSeriesFamily_subset`, `coeff_heval`, `coeff_heval_zero`, `heval_C`, `heval_X`, `heval_apply`, `heval_mul`, `heval_unit`	14
Total	16

HahnSeries.SummableFamily

Definitions

Name	Category	Theorems
`powerSeriesFamily` 📖	CompOp	9 math math: `powerSeriesFamily_add`, `PowerSeries.coeff_heval`, `powerSeriesFamily_of_not_orderTop_pos`, `hsum_powerSeriesFamily_mul`, `PowerSeries.heval_apply`, `powerSeriesFamily_hsum_zero`, `powerSeriesFamily_of_orderTop_pos`, `support_powerSeriesFamily_subset`, `powerSeriesFamily_smul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hsum_powerSeriesFamily_mul` 📖	mathematical	—	`hsum` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `powerSeriesFamily` `PowerSeries` `MvPowerSeries.instMul` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `mul`	—	`HahnSeries.ext` `coeff_hsum_eq_sum` `Finset.sum_congr` `powers_of_orderTop_pos` `Algebra.mul_smul_comm` `Algebra.smul_mul_assoc` `Finset.sum_subset` `support_powerSeriesFamily_subset` `PowerSeries.coeff_mul` `Finset.sum_smul` `finite_co_support` `HahnSeries.coeff_sum` `Set.Finite.toFinset.congr_simp` `Finset.sum_sigma'` `Finset.sum_of_injOn` `Finset.coe_sigma` `Finset.coe_image` `Set.Finite.coe_toFinset` `Mathlib.Tactic.Contrapose.contrapose₁` `mul_comm` `SemigroupAction.mul_smul` `pow_add` `Sigma.eq` `smul_smul` `powerSeriesFamily_of_not_orderTop_pos` `powerSeriesFamily_hsum_zero` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `mul.congr_simp` `hsum_mul` `smul_mul_smul_comm` `IsScalarTower.right` `HahnModule.instIsScalarTowerHahnSeries` `IsScalarTower.left` `Algebra.to_smulCommClass` `mul_one`
`powerSeriesFamily_add` 📖	mathematical	—	`powerSeriesFamily` `PowerSeries` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `PowerSeries.instCommRing` `HahnSeries.SummableFamily` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instAdd`	—	`ext` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `add_smul`
`powerSeriesFamily_hsum_zero` 📖	mathematical	—	`hsum` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `powerSeriesFamily` `HahnSeries` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `HahnSeries.instZero` `HahnSeries.instSMul` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `Algebra.toModule` `DFunLike.coe` `RingHom` `PowerSeries` `Semiring.toNonAssocSemiring` `PowerSeries.instSemiring` `RingHom.instFunLike` `PowerSeries.constantCoeff` `HahnSeries.instOne` `AddZero.toZero` `AddZeroClass.toAddZero` `AddCommMonoid.toAddMonoid` `AddMonoidWithOne.toOne`	—	`HahnSeries.ext` `finsum_eq_single` `powers_zero` `Pi.single_eq_of_ne` `smul_zero` `PowerSeries.coeff_zero_eq_constantCoeff` `Pi.single_eq_same` `HahnSeries.coeff_one` `coeff_hsum` `finsum_eq_zero_of_forall_eq_zero`
`powerSeriesFamily_of_not_orderTop_pos` 📖	mathematical	`WithTop` `Preorder.toLT` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `WithTop.zero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `HahnSeries.orderTop` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`powerSeriesFamily` `HahnSeries` `HahnSeries.instZero`	—	`ext` `HahnSeries.ext` `eq_or_ne` `PowerSeries.coeff_zero_eq_constantCoeff` `pow_zero` `HahnSeries.coeff_one` `smul_ite` `smul_zero` `powers_zero` `Pi.single_eq_same` `zero_pow` `Pi.single_eq_of_ne`
`powerSeriesFamily_of_orderTop_pos` 📖	mathematical	`WithTop` `Preorder.toLT` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `WithTop.zero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `HahnSeries.orderTop` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`DFunLike.coe` `HahnSeries.SummableFamily` `NonUnitalNonAssocSemiring.toAddCommMonoid` `HahnSeries` `instFunLike` `powerSeriesFamily` `HahnSeries.instSMul` `DistribSMul.toSMulZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `Algebra.toModule` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `PowerSeries.instAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `PowerSeries.instModule` `Semiring.toModule` `LinearMap.instFunLike` `PowerSeries.coeff` `Monoid.toNatPow` `HahnSeries.instSemiring`	—	—
`powerSeriesFamily_smul` 📖	mathematical	—	`powerSeriesFamily` `PowerSeries` `Algebra.toSMul` `CommRing.toCommSemiring` `PowerSeries.instSemiring` `CommSemiring.toSemiring` `PowerSeries.instAlgebra` `Algebra.id` `HahnSeries` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `HahnSeries.SummableFamily` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instSMul_1` `MulActionWithZero.toSMulWithZero` `Semiring.toMonoidWithZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Module.toMulActionWithZero` `Algebra.toModule` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid` `DFunLike.coe` `ZeroHom` `HahnSeries.instZero` `ZeroHom.funLike` `HahnSeries.single`	—	`ext` `instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `ite_pow` `smul_ite` `SemigroupAction.mul_smul` `HahnModule.single_zero_smul_eq_smul` `Equiv.symm_apply_apply`
`support_powerSeriesFamily_subset` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `Finsupp.support` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `coeff` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `powerSeriesFamily` `PowerSeries` `MvPowerSeries.instMul` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Finset.image` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `mul`	—	`finite_co_support` `Finset.exists_ne_zero_of_sum_ne_zero` `Finset.sum_congr` `PowerSeries.coeff_mul` `Finset.sum_smul` `SemigroupAction.mul_smul` `HahnSeries.coeff_sum` `powers_of_orderTop_pos` `Finset.coe_image` `Set.Finite.coe_toFinset` `Algebra.smul_mul_assoc` `Algebra.mul_smul_comm` `pow_add` `PowerSeries.coeff_zero_eq_constantCoeff` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `pow_zero` `HahnSeries.coeff_one` `smul_ite` `smul_zero` `mul_comm` `smul_smul` `Set.Finite.toFinset.congr_simp` `mul_one` `add_zero` `zero_pow`

PowerSeries

Definitions

Name	Category	Theorems
`heval` 📖	CompOp	7 math math: `heval_C`, `coeff_heval`, `heval_apply`, `heval_X`, `heval_unit`, `coeff_heval_zero`, `heval_mul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_heval` 📖	mathematical	—	`HahnSeries.coeff` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `AlgHom` `PowerSeries` `HahnSeries` `CommRing.toCommSemiring` `instSemiring` `CommSemiring.toSemiring` `HahnSeries.instSemiring` `instAlgebra` `Algebra.id` `HahnSeries.instAlgebra` `AlgHom.funLike` `heval` `finsum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instFunLike` `HahnSeries.SummableFamily.coeff` `HahnSeries.SummableFamily.powerSeriesFamily`	—	`heval_apply` `HahnSeries.SummableFamily.coeff_hsum`
`coeff_heval_zero` 📖	mathematical	—	`HahnSeries.coeff` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `AlgHom` `PowerSeries` `HahnSeries` `CommRing.toCommSemiring` `instSemiring` `CommSemiring.toSemiring` `HahnSeries.instSemiring` `instAlgebra` `Algebra.id` `HahnSeries.instAlgebra` `AlgHom.funLike` `heval` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `constantCoeff`	—	`coeff_heval` `finsum_eq_single` `mul_eq_zero_of_right` `HahnSeries.coeff_eq_zero_of_lt_orderTop` `lt_of_lt_of_le` `nsmul_pos_iff` `WithTop.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `zero_pow` `HahnSeries.orderTop_zero` `coeff_zero_eq_constantCoeff_apply` `coeff_zero_eq_constantCoeff` `pow_zero` `HahnSeries.coeff_one` `mul_one`
`heval_C` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `PowerSeries` `HahnSeries` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CommRing.toCommSemiring` `instSemiring` `CommSemiring.toSemiring` `HahnSeries.instSemiring` `instAlgebra` `Algebra.id` `HahnSeries.instAlgebra` `AlgHom.funLike` `heval` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C` `HahnSeries.instSMul` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `NonUnitalNonAssocSemiring.toDistribSMul` `HahnSeries.instOne` `AddZero.toZero` `AddZeroClass.toAddZero` `AddCommMonoid.toAddMonoid` `AddMonoidWithOne.toOne`	—	`HahnSeries.ext` `HahnSeries.coeff_one` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `finsum_eq_single` `coeff_ne_zero_C` `ite_pow` `MulZeroClass.zero_mul` `coeff_zero_C` `pow_zero`
`heval_X` 📖	mathematical	`WithTop` `Preorder.toLT` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `WithTop.zero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `HahnSeries.orderTop` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`DFunLike.coe` `AlgHom` `PowerSeries` `HahnSeries` `CommRing.toCommSemiring` `instSemiring` `CommSemiring.toSemiring` `HahnSeries.instSemiring` `instAlgebra` `Algebra.id` `HahnSeries.instAlgebra` `AlgHom.funLike` `heval` `X`	—	`X_eq` `heval_apply` `HahnSeries.SummableFamily.powerSeriesFamily.eq_1` `HahnSeries.SummableFamily.smulFamily.eq_1` `ite_smul` `one_smul` `zero_smul` `HahnSeries.ext` `HahnSeries.SummableFamily.coeff_hsum` `finsum_eq_single` `pow_one`
`heval_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `PowerSeries` `HahnSeries` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CommRing.toCommSemiring` `instSemiring` `CommSemiring.toSemiring` `HahnSeries.instSemiring` `instAlgebra` `Algebra.id` `HahnSeries.instAlgebra` `AlgHom.funLike` `heval` `HahnSeries.SummableFamily.hsum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `HahnSeries.SummableFamily.powerSeriesFamily`	—	—
`heval_mul` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `PowerSeries` `HahnSeries` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CommRing.toCommSemiring` `instSemiring` `CommSemiring.toSemiring` `HahnSeries.instSemiring` `instAlgebra` `Algebra.id` `HahnSeries.instAlgebra` `AlgHom.funLike` `heval` `MvPowerSeries.instMul` `HahnSeries.instMul`	—	`map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass`
`heval_unit` 📖	mathematical	—	`IsUnit` `HahnSeries` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `HahnSeries.instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `PowerSeries` `instSemiring` `instAlgebra` `Algebra.id` `HahnSeries.instAlgebra` `AlgHom.funLike` `heval` `Units.val`	—	`isUnit_iff_exists_inv` `instIsDedekindFiniteMonoid` `heval_mul` `Units.val_inv` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`

---

← Back to Index