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	42 math math: HahnEmbedding.Seed.baseEmbedding_pos, HahnEmbedding.IsPartial.baseEmbedding_le, HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk, HahnEmbedding.Partial.baseEmbedding_le_sSupFun, HahnEmbedding.Partial.archimedeanClassMk_eq_iff, HahnEmbedding.Partial.truncLT_mem_range_extendFun, HahnEmbedding.Seed.baseEmbedding_strictMono, HahnEmbedding.Partial.toOrderAddMonoidHom_apply, HahnEmbedding.Partial.orderTop_eq_iff, HahnEmbedding.Partial.lt_extend, HahnEmbedding.Partial.coeff_eq_of_mem, HahnEmbedding.Partial.extendFun_strictMono, HahnEmbedding.IsPartial.strictMono, HahnEmbedding.Partial.exists_sub_mem_ball, HahnEmbedding.IsPartial.truncLT_mem_range, HahnEmbedding.Partial.truncLT_mem_range_sSupFun, archimedeanClassMk_eq_archimedeanClassMk_iff, HahnEmbedding.Partial.le_sSupFun, finiteArchimedeanClassOrderIsoLex_apply_snd, HahnEmbedding.Seed.coeff_baseEmbedding, archimedeanClassOrderIsoWithTop_apply, archimedeanClassMk_le_archimedeanClassMk_iff_of_orderTop_ofLex, HahnEmbedding.Partial.coeff_eq_zero_of_mem, HahnEmbedding.Partial.orderTop_eq_finiteArchimedeanClassMk, HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding, HahnEmbedding.Partial.mem_domain, HahnEmbedding.Seed.mem_domain_baseEmbedding, archimedeanClassMk_le_archimedeanClassMk_iff, HahnEmbedding.Partial.eval_lt, finiteArchimedeanClassOrderIsoLex_apply_fst, HahnEmbedding.Partial.archimedeanClassMk_le_of_eval_eq, HahnEmbedding.Partial.baseEmbedding_le_extendFun, HahnEmbedding.Partial.eval_eq_truncLT, finiteArchimedeanClassOrderIso_apply, HahnEmbedding.Partial.evalCoeff_eq, HahnEmbedding.Partial.sSupFun_strictMono, HahnEmbedding.Partial.exists_domain_eq_top, HahnEmbedding.Partial.truncLT_eval_mem_range_extendFun, HahnEmbedding.Partial.exists_isMax, HahnEmbedding.Partial.apply_of_mem_stratum, 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	51 math math: HahnEmbedding.Seed.baseEmbedding_pos, HahnEmbedding.IsPartial.baseEmbedding_le, HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk, embDomainLinearMap_apply, HahnEmbedding.Partial.baseEmbedding_le_sSupFun, HahnEmbedding.Partial.archimedeanClassMk_eq_iff, single.linearMap_apply, HahnEmbedding.Partial.truncLT_mem_range_extendFun, HahnEmbedding.Seed.baseEmbedding_strictMono, HahnEmbedding.Partial.toOrderAddMonoidHom_apply, HahnEmbedding.Partial.orderTop_eq_iff, HahnEmbedding.Partial.lt_extend, HahnEmbedding.Partial.coeff_eq_of_mem, HahnEmbedding.Partial.extendFun_strictMono, coe_truncLTLinearMap, HahnEmbedding.IsPartial.strictMono, LaurentSeries.derivative_iterate_coeff, HahnEmbedding.Partial.exists_sub_mem_ball, HahnEmbedding.IsPartial.truncLT_mem_range, LaurentSeries.derivative_apply, HahnEmbedding.Partial.truncLT_mem_range_sSupFun, HahnEmbedding.Partial.le_sSupFun, LaurentSeries.hasseDeriv_comp_coeff, HahnEmbedding.Seed.coeff_baseEmbedding, LaurentSeries.hasseDeriv_coeff, LaurentSeries.hasseDeriv_single_add, LaurentSeries.hasseDeriv_comp, HahnEmbedding.Partial.coeff_eq_zero_of_mem, HahnEmbedding.Partial.orderTop_eq_finiteArchimedeanClassMk, hahnEmbedding_isOrderedModule_rat, HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding, HahnEmbedding.Partial.mem_domain, HahnEmbedding.Seed.mem_domain_baseEmbedding, HahnEmbedding.Partial.eval_lt, coeff.linearMap_apply, LaurentSeries.derivative_iterate, HahnEmbedding.Partial.archimedeanClassMk_le_of_eval_eq, HahnEmbedding.Partial.baseEmbedding_le_extendFun, LaurentSeries.hasseDeriv_zero, HahnEmbedding.Partial.eval_eq_truncLT, HahnEmbedding.Partial.evalCoeff_eq, HahnEmbedding.Partial.sSupFun_strictMono, HahnEmbedding.Partial.exists_domain_eq_top, HahnEmbedding.Partial.truncLT_eval_mem_range_extendFun, HahnEmbedding.Partial.exists_isMax, HahnEmbedding.Partial.apply_of_mem_stratum, 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	26 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.orderTop_hsum_binomialFamily_pos, SummableFamily.coe_sub, SummableFamily.one_sub_self_mul_hsum_powers, map_sub, SummableFamily.binomialFamily_apply, 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.toNSMul 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 AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid order	—	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 SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithTop.some orderTop NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid 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 SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass 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 SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass 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 SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid 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 instReflLe 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	orderTop SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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	orderTop SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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	orderTop SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder order AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCancelCommMonoid.toAddCommMonoid	—	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