Addition

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

Statistics

Metric	Count
Definitions `addOppositeEquiv`, `addMonoidHom`, `linearMap`, `embDomainLinearMap`, `instAdd`, `instAddCommGroup`, `instAddCommMonoid`, `instAddGroup`, `instAddMonoid`, `instDistribMulAction`, `instModule`, `instNeg`, `instSMul`, `instSMulZeroClass`, `instSub`, `ofFinsuppLinearMap`, `addMonoidHom`, `linearMap`, `truncLTLinearMap`	19
Theorems `addOppositeEquiv_apply`, `addOppositeEquiv_leadingCoeff`, `addOppositeEquiv_orderTop`, `addOppositeEquiv_support`, `addOppositeEquiv_symm_apply_coeff`, `addOppositeEquiv_symm_leadingCoeff`, `addOppositeEquiv_symm_orderTop`, `addOppositeEquiv_symm_support`, `coe_truncLTLinearMap`, `addMonoidHom_apply`, `linearMap_apply`, `coeff_add`, `coeff_add'`, `coeff_neg`, `coeff_neg'`, `coeff_nsmul`, `coeff_ofFinsuppLinearMap`, `coeff_order_of_eq_add_single`, `coeff_smul`, `coeff_smul'`, `coeff_sub`, `coeff_sub'`, `coeff_sum`, `embDomainLinearMap_apply`, `embDomain_add`, `embDomain_smul`, `instIsScalarTower`, `instSMulCommClass`, `le_orderTop_of_leadingCoeff_eq`, `le_order_smul`, `leadingCoeff_add_eq_left`, `leadingCoeff_add_eq_right`, `leadingCoeff_neg`, `leadingCoeff_sub`, `map_add`, `map_neg`, `map_smul`, `map_sub`, `min_le_min_add`, `min_orderTop_le_orderTop_add`, `min_orderTop_le_orderTop_sub`, `min_order_le_order_add`, `ne_zero_of_eq_add_single`, `orderTop_add_eq_left`, `orderTop_add_eq_right`, `orderTop_le_orderTop_smul`, `orderTop_neg`, `orderTop_smul_not_lt`, `orderTop_sub`, `orderTop_sub_ne`, `order_lt_order_of_eq_add_single`, `order_neg`, `order_smul_not_lt`, `addMonoidHom_apply_coeff`, `linearMap_apply`, `single_add`, `single_neg`, `single_sub`, `support_add_subset`, `support_neg`, `support_neg_subset`, `support_smul_subset`, `support_sub_subset`, `truncLT_add`, `truncLT_smul`	65
Total	84

HahnSeries

Definitions

Name	Category	Theorems
`addOppositeEquiv` 📖	CompOp	8 math math: `addOppositeEquiv_symm_support`, `addOppositeEquiv_support`, `addOppositeEquiv_orderTop`, `addOppositeEquiv_symm_orderTop`, `addOppositeEquiv_symm_leadingCoeff`, `addOppositeEquiv_leadingCoeff`, `addOppositeEquiv_symm_apply_coeff`, `addOppositeEquiv_apply`
`embDomainLinearMap` 📖	CompOp	1 math math: `embDomainLinearMap_apply`
`instAdd` 📖	CompOp	49 math math: `LaurentSeries.LaurentSeriesRingEquiv_def`, `addOppositeEquiv_symm_support`, `orderTop_sub_pos`, `SummableFamily.coe_add`, `SummableFamily.add_apply`, `HahnModule.add_smul`, `PowerSeries.coe_add`, `toMvPowerSeries_symm_apply_coeff`, `addOppositeEquiv_support`, `SummableFamily.hsum_add`, `truncLT_add`, `LaurentSeries.coe_X_compare`, `HVertexOperator.compHahnSeries_add`, `min_order_le_order_add`, `LaurentSeries.exists_powerSeries_of_memIntegers`, `HahnModule.of_symm_add`, `addOppositeEquiv_orderTop`, `coeff_toPowerSeries`, `embDomain_add`, `LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring`, `single_add`, `coeff_toPowerSeries_symm`, `LaurentSeries.powerSeriesRingEquiv_coe_apply`, `coeff_add`, `addOppositeEquiv_symm_orderTop`, `coeff_toMvPowerSeries_symm`, `addOppositeEquiv_symm_leadingCoeff`, `addOppositeEquiv_leadingCoeff`, `coeff_toMvPowerSeries`, `cardSupp_add_le`, `map_add`, `HahnModule.of_add`, `leadingCoeff_add_eq_right`, `ofPowerSeries_apply`, `toMvPowerSeries_apply`, `coeff_toOrderTopSubOnePos_pow`, `addOppositeEquiv_symm_apply_coeff`, `LaurentSeries.ratfuncAdicComplRingEquiv_apply`, `min_le_min_add`, `orderTop_add_eq_left`, `addOppositeEquiv_apply`, `orderTop_add_eq_right`, `support_add_subset`, `leadingCoeff_add_eq_left`, `LaurentSeries.mem_integers_of_powerSeries`, `toPowerSeries_apply`, `toPowerSeries_symm_apply_coeff`, `coeff_add'`, `min_orderTop_le_orderTop_add`
`instAddCommGroup` 📖	CompOp	23 math math: `HahnEmbedding.IsPartial.baseEmbedding_le`, `HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk`, `HahnEmbedding.Partial.archimedeanClassMk_eq_iff`, `HahnEmbedding.Seed.baseEmbedding_strictMono`, `HahnEmbedding.Partial.toOrderAddMonoidHom_apply`, `HahnEmbedding.Partial.orderTop_eq_iff`, `HahnEmbedding.IsPartial.strictMono`, `HahnEmbedding.IsPartial.truncLT_mem_range`, `archimedeanClassMk_eq_archimedeanClassMk_iff`, `finiteArchimedeanClassOrderIsoLex_apply_snd`, `archimedeanClassOrderIsoWithTop_apply`, `archimedeanClassMk_le_archimedeanClassMk_iff_of_orderTop_ofLex`, `HahnEmbedding.Partial.orderTop_eq_finiteArchimedeanClassMk`, `HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding`, `HahnEmbedding.Partial.mem_domain`, `HahnEmbedding.Seed.mem_domain_baseEmbedding`, `archimedeanClassMk_le_archimedeanClassMk_iff`, `finiteArchimedeanClassOrderIsoLex_apply_fst`, `finiteArchimedeanClassOrderIso_apply`, `HahnEmbedding.Partial.exists_domain_eq_top`, `HahnEmbedding.Partial.exists_isMax`, `HahnEmbedding.Seed.domain_baseEmbedding`, `HahnEmbedding.Partial.toOrderAddMonoidHom_injective`
`instAddCommMonoid` 📖	CompOp	26 math math: `embDomainLinearMap_apply`, `SummableFamily.lsum_apply`, `single.linearMap_apply`, `HahnEmbedding.Partial.truncLT_mem_range_extendFun`, `coe_truncLTLinearMap`, `LaurentSeries.derivative_iterate_coeff`, `coeff_sum`, `HahnEmbedding.IsPartial.truncLT_mem_range`, `LaurentSeries.derivative_apply`, `HahnEmbedding.Partial.truncLT_mem_range_sSupFun`, `LaurentSeries.hasseDeriv_comp_coeff`, `SummableFamily.hsum_ofFinsupp`, `LaurentSeries.hasseDeriv_coeff`, `LaurentSeries.hasseDeriv_single_add`, `LaurentSeries.hasseDeriv_comp`, `hahnEmbedding_isOrderedModule_rat`, `HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding`, `instIsOrderedAddMonoidLex`, `coeff.linearMap_apply`, `LaurentSeries.derivative_iterate`, `LaurentSeries.hasseDeriv_zero`, `HahnEmbedding.Partial.eval_eq_truncLT`, `HahnEmbedding.Partial.truncLT_eval_mem_range_extendFun`, `LaurentSeries.hasseDeriv_single`, `coeff_ofFinsuppLinearMap`, `hahnEmbedding_isOrderedModule`
`instAddGroup` 📖	CompOp	8 math math: `support_abs`, `abs_lt_abs_of_orderTop_ofLex`, `cardSuppLTSubfield_carrier`, `mem_cardSuppLTAddSubgroup`, `order_abs`, `coe_cardSuppLTAddSubgroup`, `orderTop_abs`, `leadingCoeff_abs`
`instAddMonoid` 📖	CompOp	16 math math: `coe_cardSuppLTAddSubmonoid`, `single.addMonoidHom_apply_coeff`, `single.linearMap_apply`, `HahnEmbedding.Partial.toOrderAddMonoidHom_apply`, `LaurentSeries.hasseDeriv_comp_coeff`, `HVertexOperator.compHahnSeries_add`, `embDomainOrderAddMonoidHom_injective`, `LaurentSeries.hasseDeriv_comp`, `mem_cardSuppLTAddSubmonoid`, `embDomainOrderAddMonoidHom_apply`, `coeff.linearMap_apply`, `LaurentSeries.derivative_iterate`, `coeff_nsmul`, `coeff.addMonoidHom_apply`, `hahnEmbedding_isOrderedAddMonoid`, `HahnEmbedding.Partial.toOrderAddMonoidHom_injective`
`instDistribMulAction` 📖	CompOp	—
`instModule` 📖	CompOp	32 math math: `HahnEmbedding.IsPartial.baseEmbedding_le`, `HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk`, `embDomainLinearMap_apply`, `HahnEmbedding.Partial.archimedeanClassMk_eq_iff`, `single.linearMap_apply`, `HahnEmbedding.Seed.baseEmbedding_strictMono`, `HahnEmbedding.Partial.toOrderAddMonoidHom_apply`, `HahnEmbedding.Partial.orderTop_eq_iff`, `coe_truncLTLinearMap`, `HahnEmbedding.IsPartial.strictMono`, `LaurentSeries.derivative_iterate_coeff`, `HahnEmbedding.IsPartial.truncLT_mem_range`, `LaurentSeries.derivative_apply`, `LaurentSeries.hasseDeriv_comp_coeff`, `LaurentSeries.hasseDeriv_coeff`, `LaurentSeries.hasseDeriv_single_add`, `LaurentSeries.hasseDeriv_comp`, `HahnEmbedding.Partial.orderTop_eq_finiteArchimedeanClassMk`, `hahnEmbedding_isOrderedModule_rat`, `HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding`, `HahnEmbedding.Partial.mem_domain`, `HahnEmbedding.Seed.mem_domain_baseEmbedding`, `coeff.linearMap_apply`, `LaurentSeries.derivative_iterate`, `LaurentSeries.hasseDeriv_zero`, `HahnEmbedding.Partial.exists_domain_eq_top`, `HahnEmbedding.Partial.exists_isMax`, `HahnEmbedding.Seed.domain_baseEmbedding`, `LaurentSeries.hasseDeriv_single`, `coeff_ofFinsuppLinearMap`, `hahnEmbedding_isOrderedModule`, `HahnEmbedding.Partial.toOrderAddMonoidHom_injective`
`instNeg` 📖	CompOp	15 math math: `support_neg_subset`, `order_neg`, `SummableFamily.coe_neg`, `map_neg`, `one_minus_single_neg_mul`, `cardSupp_neg_le`, `coeff_neg`, `cardSupp_neg`, `support_neg`, `single_neg`, `PowerSeries.coe_neg`, `SummableFamily.neg_apply`, `coeff_neg'`, `orderTop_neg`, `leadingCoeff_neg`
`instSMul` 📖	CompOp	29 math math: `PowerSeries.heval_C`, `cardSupp_smul_le`, `embDomain_smul`, `instSMulCommClass`, `single_zero_mul_eq_smul`, `SummableFamily.smul_apply'`, `PowerSeries.coe_smul`, `coeff_smul`, `SummableFamily.coe_smul'`, `coeff_smul'`, `HVertexOperator.compHahnSeries_smul`, `HahnModule.of_symm_smul`, `HahnModule.instIsScalarTowerHahnSeries_1`, `SummableFamily.powerSeriesFamily_hsum_zero`, `HahnEmbedding.Partial.eval_smul`, `support_smul_subset`, `order_smul_not_lt`, `SummableFamily.smulFamily_toFun`, `SummableFamily.binomialFamily_apply`, `orderTop_le_orderTop_smul`, `C_mul_eq_smul`, `SummableFamily.powerSeriesFamily_of_orderTop_pos`, `HahnModule.of_smul`, `instIsScalarTower`, `map_smul`, `HahnModule.instIsScalarTowerHahnSeries`, `truncLT_smul`, `orderTop_smul_not_lt`, `le_order_smul`
`instSMulZeroClass` 📖	CompOp	1 math math: `HVertexOperator.compHahnSeries_smul`
`instSub` 📖	CompOp	24 math math: `support_sub_subset`, `orderTop_sub_pos`, `SummableFamily.sub_apply`, `le_orderTop_of_leadingCoeff_eq`, `single_sub`, `one_minus_single_neg_mul`, `coeff_sub`, `PowerSeries.coe_sub`, `LaurentSeries.exists_ratFunc_val_lt`, `leadingCoeff_sub`, `unit_aux`, `SummableFamily.coe_sub`, `SummableFamily.one_sub_self_mul_hsum_powers`, `map_sub`, `coeff_sub'`, `inv_def`, `orderTop_self_sub_one_pos_iff`, `min_orderTop_le_orderTop_sub`, `HahnModule.of_sub`, `cardSupp_sub_le`, `SummableFamily.hsum_sub`, `mem_orderTopSubOnePos_iff`, `orderTop_sub`, `HahnModule.of_symm_sub`
`ofFinsuppLinearMap` 📖	CompOp	1 math math: `coeff_ofFinsuppLinearMap`
`truncLTLinearMap` 📖	CompOp	7 math math: `HahnEmbedding.Partial.truncLT_mem_range_extendFun`, `coe_truncLTLinearMap`, `HahnEmbedding.IsPartial.truncLT_mem_range`, `HahnEmbedding.Partial.truncLT_mem_range_sSupFun`, `HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding`, `HahnEmbedding.Partial.eval_eq_truncLT`, `HahnEmbedding.Partial.truncLT_eval_mem_range_extendFun`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addOppositeEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `HahnSeries` `AddOpposite` `AddOpposite.instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAdd` `AddOpposite.instAddMonoid` `AddOpposite.instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `addOppositeEquiv` `AddOpposite.op` `AddOpposite.unop` `coeff`	—	—
`addOppositeEquiv_leadingCoeff` 📖	mathematical	—	`leadingCoeff` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddOpposite.unop` `HahnSeries` `DFunLike.coe` `AddEquiv` `AddOpposite` `AddOpposite.instZero` `instAdd` `AddOpposite.instAddMonoid` `AddOpposite.instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `addOppositeEquiv`	—	`eq_or_ne` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `leadingCoeff_zero` `orderTop_ne_top` `EquivLike.toEmbeddingLike` `addOppositeEquiv_orderTop` `leadingCoeff_of_ne_zero` `WithTop.untop.congr_simp`
`addOppositeEquiv_orderTop` 📖	mathematical	—	`orderTop` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddOpposite.unop` `HahnSeries` `DFunLike.coe` `AddEquiv` `AddOpposite` `AddOpposite.instZero` `instAdd` `AddOpposite.instAddMonoid` `AddOpposite.instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `addOppositeEquiv`	—	`isWF_support` `addOppositeEquiv_support` `Set.IsWF.min.congr_simp`
`addOppositeEquiv_support` 📖	mathematical	—	`support` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddOpposite.unop` `HahnSeries` `DFunLike.coe` `AddEquiv` `AddOpposite` `AddOpposite.instZero` `instAdd` `AddOpposite.instAddMonoid` `AddOpposite.instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `addOppositeEquiv`	—	`Set.ext`
`addOppositeEquiv_symm_apply_coeff` 📖	mathematical	—	`coeff` `AddOpposite` `AddOpposite.instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFunLike.coe` `AddEquiv` `HahnSeries` `AddOpposite.instAdd` `instAdd` `AddOpposite.instAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `addOppositeEquiv` `AddOpposite.op` `AddOpposite.unop`	—	—
`addOppositeEquiv_symm_leadingCoeff` 📖	mathematical	—	`leadingCoeff` `AddOpposite` `AddOpposite.instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFunLike.coe` `AddEquiv` `HahnSeries` `AddOpposite.instAdd` `instAdd` `AddOpposite.instAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `addOppositeEquiv` `AddOpposite.op` `AddOpposite.unop`	—	`AddOpposite.unop_injective` `addOppositeEquiv_leadingCoeff` `AddEquiv.apply_symm_apply` `AddOpposite.unop_op`
`addOppositeEquiv_symm_orderTop` 📖	mathematical	—	`orderTop` `AddOpposite` `AddOpposite.instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFunLike.coe` `AddEquiv` `HahnSeries` `AddOpposite.instAdd` `instAdd` `AddOpposite.instAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `addOppositeEquiv` `AddOpposite.unop`	—	`addOppositeEquiv_orderTop` `AddEquiv.apply_symm_apply`
`addOppositeEquiv_symm_support` 📖	mathematical	—	`support` `AddOpposite` `AddOpposite.instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFunLike.coe` `AddEquiv` `HahnSeries` `AddOpposite.instAdd` `instAdd` `AddOpposite.instAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `addOppositeEquiv` `AddOpposite.unop`	—	`addOppositeEquiv_support` `AddEquiv.apply_symm_apply`
`coe_truncLTLinearMap` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `HahnSeries` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `instModule` `LinearMap.instFunLike` `truncLTLinearMap` `ZeroHom` `instZero` `ZeroHom.funLike` `truncLT`	—	—
`coeff_add` 📖	mathematical	—	`coeff` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `HahnSeries` `instAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	—	—
`coeff_add'` 📖	mathematical	—	`coeff` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `HahnSeries` `instAdd` `Pi.instAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	—	—
`coeff_neg` 📖	mathematical	—	`coeff` `NegZeroClass.toZero` `HahnSeries` `instNeg` `NegZeroClass.toNeg`	—	—
`coeff_neg'` 📖	mathematical	—	`coeff` `NegZeroClass.toZero` `HahnSeries` `instNeg` `Pi.instNeg` `NegZeroClass.toNeg`	—	—
`coeff_nsmul` 📖	mathematical	—	`coeff` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `HahnSeries` `AddMonoid.toNatSMul` `instAddMonoid` `Pi.addMonoid`	—	`coeff_smul'`
`coeff_ofFinsuppLinearMap` 📖	mathematical	—	`coeff` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `HahnSeries` `Finsupp.instAddCommMonoid` `instAddCommMonoid` `Finsupp.module` `instModule` `LinearMap.instFunLike` `ofFinsuppLinearMap` `Finsupp.instFunLike`	—	—
`coeff_order_of_eq_add_single` 📖	mathematical	`HahnSeries` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `instAdd` `DFunLike.coe` `ZeroHom` `instZero` `ZeroHom.funLike` `single` `order` `leadingCoeff`	`coeff`	—	`coeff_single_same` `AddRightCancelSemigroup.toIsRightCancelAdd`
`coeff_smul` 📖	mathematical	—	`coeff` `HahnSeries` `instSMul` `SMulZeroClass.toSMul`	—	—
`coeff_smul'` 📖	mathematical	—	`coeff` `HahnSeries` `instSMul` `Function.hasSMul` `SMulZeroClass.toSMul`	—	—
`coeff_sub` 📖	mathematical	—	`coeff` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `HahnSeries` `instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	—
`coeff_sub'` 📖	mathematical	—	`coeff` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `HahnSeries` `instSub` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	—
`coeff_sum` 📖	mathematical	—	`coeff` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finset.sum` `HahnSeries` `instAddCommMonoid`	—	`Finset.cons_induction` `Finset.sum_cons` `coeff_add`
`embDomainLinearMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `HahnSeries` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instModule` `Semiring.toModule` `LinearMap.instFunLike` `embDomainLinearMap` `embDomain`	—	—
`embDomain_add` 📖	mathematical	—	`embDomain` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `HahnSeries` `instAdd`	—	`ext` `embDomain_coeff` `embDomain_notin_range` `add_zero`
`embDomain_smul` 📖	mathematical	—	`embDomain` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `HahnSeries` `instSMul` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `instDistribSMul`	—	`ext` `embDomain_coeff` `embDomain_notin_range` `MulZeroClass.mul_zero`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `HahnSeries` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	`ext` `smul_assoc`
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `HahnSeries` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	`ext` `SMulCommClass.smul_comm`
`le_orderTop_of_leadingCoeff_eq` 📖	mathematical	`orderTop` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `WithTop.some` `leadingCoeff`	`WithTop` `Preorder.toLT` `WithTop.instPreorder` `PartialOrder.toPreorder` `HahnSeries` `instSub`	—	`lt_of_le_of_ne` `inf_idem` `min_orderTop_le_orderTop_sub` `orderTop_sub_ne`
`le_order_smul` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `order` `HahnSeries` `instSMul`	—	`le_of_not_gt` `order_smul_not_lt`
`leadingCoeff_add_eq_left` 📖	mathematical	`WithTop` `Preorder.toLT` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `orderTop` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`leadingCoeff` `HahnSeries` `instAdd`	—	`orderTop_ne_top` `LT.lt.ne_top` `orderTop_add_eq_left` `orderTop_eq_top` `orderTop_zero` `leadingCoeff_of_ne_zero` `WithTop.untop.congr_simp` `coeff_eq_zero_of_lt_orderTop` `WithTop.coe_untop` `add_zero`
`leadingCoeff_add_eq_right` 📖	mathematical	`WithTop` `Preorder.toLT` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `orderTop` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`leadingCoeff` `HahnSeries` `instAdd`	—	`addOppositeEquiv_symm_orderTop` `AddMonoidHomClass.toAddHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `addOppositeEquiv_symm_leadingCoeff` `leadingCoeff_add_eq_left`
`leadingCoeff_neg` 📖	mathematical	—	`leadingCoeff` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `HahnSeries` `instNeg` `NegZeroClass.toNeg`	—	`eq_or_ne` `neg_zero` `leadingCoeff_zero` `orderTop_ne_top` `orderTop_neg` `leadingCoeff_of_ne_zero` `WithTop.untop.congr_simp`
`leadingCoeff_sub` 📖	mathematical	`WithTop` `Preorder.toLT` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `orderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`leadingCoeff` `HahnSeries` `instSub`	—	`sub_eq_add_neg` `leadingCoeff_add_eq_left` `orderTop_neg`
`map_add` 📖	mathematical	—	`map` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `HahnSeries` `instAdd` `AddMonoidHom` `AddMonoidHom.instFunLike` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass`	—	`ext` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `map_add` `AddMonoidHomClass.toAddHomClass`
`map_neg` 📖	mathematical	—	`map` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `HahnSeries` `instNeg` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `AddZero.toZero`	—	`ext` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `map_neg`
`map_smul` 📖	mathematical	—	`map` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `HahnSeries` `instSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`	—	`ext` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass`
`map_sub` 📖	mathematical	—	`map` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `HahnSeries` `instSub` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `AddZero.toZero`	—	`ext` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `map_sub`
`min_le_min_add` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeInf.toMin` `Set.IsWF.min` `support` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `isWF_support` `Set.Nonempty` `HahnSeries` `instZero` `support_nonempty_iff` `instAdd`	—	`isWF_support` `support_nonempty_iff` `Set.IsWF.union` `Set.union_nonempty` `Set.IsWF.min_union` `Set.IsWF.min_le_min_of_subset` `support_add_subset`
`min_orderTop_le_orderTop_add` 📖	mathematical	—	`WithTop` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeInf.toMin` `WithTop.semilatticeInf` `orderTop` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `HahnSeries` `instAdd`	—	`orderTop_zero` `inf_of_le_right` `zero_add` `inf_of_le_left` `add_zero` `isWF_support` `support_nonempty_iff` `orderTop_of_ne_zero` `WithTop.coe_min` `WithTop.coe_le_coe` `min_le_min_add`
`min_orderTop_le_orderTop_sub` 📖	mathematical	—	`WithTop` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeInf.toMin` `WithTop.semilatticeInf` `orderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `HahnSeries` `instSub`	—	`sub_eq_add_neg` `orderTop_neg` `min_orderTop_le_orderTop_add`
`min_order_le_order_add` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeInf.toMin` `order` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `HahnSeries` `instAdd`	—	`order_zero` `zero_add` `add_zero` `isWF_support` `support_nonempty_iff` `order_of_ne` `min_le_min_add`
`ne_zero_of_eq_add_single` 📖	—	`HahnSeries` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAdd` `DFunLike.coe` `ZeroHom` `instZero` `ZeroHom.funLike` `single` `order` `leadingCoeff`	—	—	`order_zero` `leadingCoeff_zero` `map_zero` `ZeroHom.zeroHomClass` `add_zero`
`orderTop_add_eq_left` 📖	mathematical	`WithTop` `Preorder.toLT` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `orderTop` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`HahnSeries` `instAdd`	—	`orderTop_ne_top` `LT.lt.ne_top` `isWF_support` `support_nonempty_iff` `coeff_add` `coeff_eq_zero_of_lt_orderTop` `orderTop_of_ne_zero` `add_zero` `coeff_orderTop_ne` `orderTop_le_of_coeff_ne_zero` `le_antisymm` `min_eq_left_of_lt` `min_orderTop_le_orderTop_add`
`orderTop_add_eq_right` 📖	mathematical	`WithTop` `Preorder.toLT` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `orderTop` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`HahnSeries` `instAdd`	—	`addOppositeEquiv_symm_orderTop` `AddMonoidHomClass.toAddHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `orderTop_add_eq_left`
`orderTop_le_orderTop_smul` 📖	mathematical	—	`WithTop` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `orderTop` `HahnSeries` `instSMul`	—	`le_of_not_gt` `orderTop_smul_not_lt`
`orderTop_neg` 📖	mathematical	—	`orderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `HahnSeries` `instNeg`	—	`isWF_support` `support_neg` `Set.IsWF.min.congr_simp`
`orderTop_smul_not_lt` 📖	mathematical	—	`WithTop` `Preorder.toLT` `WithTop.instPreorder` `PartialOrder.toPreorder` `orderTop` `HahnSeries` `instSMul`	—	`orderTop_zero` `not_top_lt` `isWF_support` `support_nonempty_iff` `right_ne_zero_of_smul` `orderTop_of_ne_zero` `Set.IsWF.min_of_subset_not_lt_min` `Function.support_smul_subset_right`
`orderTop_sub` 📖	mathematical	`WithTop` `Preorder.toLT` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `orderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`HahnSeries` `instSub`	—	`sub_eq_add_neg` `orderTop_add_eq_left` `orderTop_neg`
`orderTop_sub_ne` 📖	—	`orderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `WithTop.some` `leadingCoeff`	—	—	`orderTop_ne_of_coeff_eq_zero` `orderTop_zero` `coeff_sub` `sub_eq_zero` `orderTop_ne_top` `leadingCoeff_of_ne_zero` `isWF_support` `support_nonempty_iff` `untop_orderTop_of_ne_zero` `WithTop.coe_eq_coe` `orderTop_of_ne_zero`
`order_lt_order_of_eq_add_single` 📖	mathematical	`HahnSeries` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `instAdd` `DFunLike.coe` `ZeroHom` `instZero` `ZeroHom.funLike` `single` `order` `leadingCoeff`	`Preorder.toLT` `PartialOrder.toPreorder`	—	`single_ne_zero` `leadingCoeff_ne_zero` `single_eq_zero` `coeff_order_of_eq_add_single` `leadingCoeff_eq` `lt_of_le_of_ne` `isWF_support` `ne_zero_of_eq_add_single` `Set.IsWF.min_le_min_of_subset` `eq_or_ne` `Iff.not` `coeff_order_eq_zero` `add_zero` `coeff_single_of_ne` `coeff_add`
`order_neg` 📖	mathematical	—	`order` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `HahnSeries` `instNeg`	—	`neg_zero` `isWF_support` `support_neg` `Set.IsWF.min.congr_simp`
`order_smul_not_lt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `order` `HahnSeries` `instSMul`	—	`right_ne_zero_of_smul` `isWF_support` `Set.IsWF.min_of_subset_not_lt_min` `Function.support_smul_subset_right`
`single_add` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `HahnSeries` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instZero` `ZeroHom.funLike` `single` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `instAdd`	—	`ext` `Pi.single_add`
`single_neg` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `HahnSeries` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `instZero` `ZeroHom.funLike` `single` `NegZeroClass.toNeg` `instNeg`	—	`map_neg` `AddMonoidHom.instAddMonoidHomClass`
`single_sub` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `HahnSeries` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `instZero` `ZeroHom.funLike` `single` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `instSub`	—	`map_sub` `AddMonoidHom.instAddMonoidHomClass`
`support_add_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `support` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `HahnSeries` `instAdd` `Set.instUnion`	—	`Function.support_add`
`support_neg` 📖	mathematical	—	`support` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `HahnSeries` `instNeg`	—	`Set.ext`
`support_neg_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `support` `NegZeroClass.toZero` `HahnSeries` `instNeg`	—	`support_map_subset`
`support_smul_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `support` `HahnSeries` `instSMul`	—	`Function.support_const_smul_subset`
`support_sub_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `support` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `HahnSeries` `instSub` `Set.instUnion`	—	`Function.support_sub`
`truncLT_add` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `HahnSeries` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instZero` `ZeroHom.funLike` `truncLT` `instAdd`	—	`ext` `add_zero`
`truncLT_smul` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `HahnSeries` `instZero` `ZeroHom.funLike` `truncLT` `instSMul`	—	`ext` `smul_ite` `smul_zero`

HahnSeries.coeff

Definitions

Name	Category	Theorems
`addMonoidHom` 📖	CompOp	2 math math: `linearMap_apply`, `addMonoidHom_apply`
`linearMap` 📖	CompOp	1 math math: `linearMap_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `HahnSeries` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `HahnSeries.instAddMonoid` `AddMonoidHom.instFunLike` `addMonoidHom` `HahnSeries.coeff`	—	—
`linearMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `HahnSeries` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `HahnSeries.instAddCommMonoid` `HahnSeries.instModule` `LinearMap.instFunLike` `linearMap` `ZeroHom.toFun` `HahnSeries.instAddMonoid` `AddMonoidHom.toZeroHom` `addMonoidHom`	—	—

HahnSeries.single

Definitions

Name	Category	Theorems
`addMonoidHom` 📖	CompOp	2 math math: `addMonoidHom_apply_coeff`, `linearMap_apply`
`linearMap` 📖	CompOp	1 math math: `linearMap_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addMonoidHom_apply_coeff` 📖	mathematical	—	`HahnSeries.coeff` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFunLike.coe` `AddMonoidHom` `HahnSeries` `HahnSeries.instAddMonoid` `AddMonoidHom.instFunLike` `addMonoidHom` `Pi.single`	—	—
`linearMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `HahnSeries` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `HahnSeries.instAddCommMonoid` `HahnSeries.instModule` `LinearMap.instFunLike` `linearMap` `ZeroHom.toFun` `HahnSeries.instAddMonoid` `AddMonoidHom.toZeroHom` `addMonoidHom`	—	—

---

← Back to Index