Multiplication

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

Statistics

Metric	Count
Definitions `HahnModule`, `instAddCommGroup`, `instAddCommMonoid`, `instBaseModule`, `instBaseSMul`, `instBaseSMulZeroClass`, `instDistribSMul`, `instModule`, `instSMul`, `instSMulZeroClass`, `instZero`, `of`, `rec`, `C`, `embDomainAlgHom`, `embDomainRingHom`, `instAddCommGroupWithOne`, `instAddCommMonoidWithOne`, `instAlgebra`, `instCommRing`, `instCommSemiring`, `instDistrib`, `instIntCast`, `instMul`, `instNNRatCast`, `instNatCast`, `instNonAssocRing`, `instNonAssocSemiring`, `instNonUnitalCommRing`, `instNonUnitalCommSemiring`, `instNonUnitalNonAssocRing`, `instNonUnitalNonAssocSemiring`, `instNonUnitalRing`, `instNonUnitalSemiring`, `instOne`, `instRatCast`, `instRing`, `instSemiring`, `orderTopSubOnePos`	39
Theorems `SMulCommClass`, `add_smul`, `coeff_single_smul_vadd`, `coeff_single_zero_smul`, `coeff_smul`, `coeff_smul_left`, `coeff_smul_order_add_order`, `coeff_smul_right`, `ext`, `ext_iff`, `instIsScalarTowerHahnSeries`, `instIsScalarTowerHahnSeries_1`, `instIsTorsionFree`, `of_add`, `of_smul`, `of_sub`, `of_symm_add`, `of_symm_smul`, `of_symm_sub`, `of_symm_zero`, `of_zero`, `one_smul'`, `orderTop_vAdd_le_orderTop_smul`, `single_zero_smul_eq_smul`, `smul_add`, `support_smul_subset_vadd_support`, `support_smul_subset_vadd_support'`, `zero_smul'`, `C_apply`, `C_eq_algebraMap`, `C_injective`, `C_mul_eq_smul`, `C_ne_zero`, `C_one`, `C_zero`, `algebraMap_apply`, `coeff_mul`, `coeff_mul_left'`, `coeff_mul_order_add_order`, `coeff_mul_right'`, `coeff_mul_single`, `coeff_mul_single_add`, `coeff_mul_single_zero`, `coeff_one`, `coeff_single_mul`, `coeff_single_mul_add`, `coeff_single_zero_mul`, `embDomainAlgHom_apply_coeff`, `embDomainRingHom_C`, `embDomainRingHom_apply`, `embDomain_mul`, `embDomain_one`, `instIsCancelMulZeroOfIsCancelAdd`, `instIsDomainOfIsCancelAdd`, `instNoZeroDivisors`, `instNontrivialSubalgebra`, `leadingCoeff_mul`, `leadingCoeff_mul_of_ne_zero`, `leadingCoeff_mul_of_nonzero`, `leadingCoeff_one`, `map_C`, `map_mul`, `map_one`, `mem_orderTopSubOnePos_iff`, `of_symm_smul_of_eq_mul`, `orderTop_add_le_mul`, `orderTop_mul`, `orderTop_mul_of_ne_zero`, `orderTop_mul_of_nonzero`, `orderTop_nsmul_le_orderTop_pow`, `orderTop_one`, `orderTop_self_sub_one_pos_iff`, `orderTop_sub_pos`, `order_C`, `order_mul`, `order_mul_of_ne_zero`, `order_mul_of_nonzero`, `order_one`, `order_pow`, `order_single_mul_of_isRegular`, `single_mul_single`, `single_pow`, `single_zero_intCast`, `single_zero_mul_eq_smul`, `single_zero_natCast`, `single_zero_nnratCast`, `single_zero_ofNat`, `single_zero_one`, `single_zero_ratCast`, `support_mul_subset`, `support_mul_subset_add_support`, `support_one`	92
Total	131

HahnModule

Definitions

Name	Category	Theorems
`instAddCommGroup` 📖	CompOp	2 math math: `of_sub`, `of_symm_sub`
`instAddCommMonoid` 📖	CompOp	21 math math: `smul_add`, `VertexOperator.of_coeff_apply_coeff`, `HVertexOperator.coeff_isPWOsupport`, `add_smul`, `VertexOperator.ncoeff_apply`, `HVertexOperator.of_coeff_coeff`, `HVertexOperator.coeff_inj_iff`, `of_symm_add`, `HVertexOperator.coeff_inj`, `VertexOperator.ext_iff`, `HVertexOperator.ext_iff`, `of_add`, `VertexOperator.ncoeff_of_coeff`, `HVertexOperator.compHahnSeries_coeff`, `HVertexOperator.coeff_comp`, `HVertexOperator.coeff_apply_apply`, `HVertexOperator.of_coeff_apply`, `instIsTorsionFree`, `VertexOperator.coeff_eq_ncoeff`, `HVertexOperator.comp_apply`, `HVertexOperator.coeff_of_coeff`
`instBaseModule` 📖	CompOp	16 math math: `VertexOperator.of_coeff_apply_coeff`, `HVertexOperator.coeff_isPWOsupport`, `VertexOperator.ncoeff_apply`, `HVertexOperator.of_coeff_coeff`, `HVertexOperator.coeff_inj_iff`, `HVertexOperator.coeff_inj`, `VertexOperator.ext_iff`, `HVertexOperator.ext_iff`, `VertexOperator.ncoeff_of_coeff`, `HVertexOperator.compHahnSeries_coeff`, `HVertexOperator.coeff_comp`, `HVertexOperator.coeff_apply_apply`, `HVertexOperator.of_coeff_apply`, `VertexOperator.coeff_eq_ncoeff`, `HVertexOperator.comp_apply`, `HVertexOperator.coeff_of_coeff`
`instBaseSMul` 📖	CompOp	2 math math: `instIsScalarTowerHahnSeries_1`, `SMulCommClass`
`instBaseSMulZeroClass` 📖	CompOp	3 math math: `of_symm_smul`, `of_smul`, `single_zero_smul_eq_smul`
`instDistribSMul` 📖	CompOp	—
`instModule` 📖	CompOp	1 math math: `instIsTorsionFree`
`instSMul` 📖	CompOp	21 math math: `support_smul_subset_vadd_support'`, `smul_add`, `coeff_single_smul_vadd`, `add_smul`, `HahnSeries.SummableFamily.hsum_smul_module`, `HahnSeries.SummableFamily.smul_apply`, `HahnSeries.SummableFamily.smul_hsum`, `HahnSeries.of_symm_smul_of_eq_mul`, `HahnSeries.SummableFamily.smul_toFun`, `coeff_smul_order_add_order`, `instIsScalarTowerHahnSeries_1`, `SMulCommClass`, `coeff_smul`, `coeff_single_zero_smul`, `orderTop_vAdd_le_orderTop_smul`, `zero_smul'`, `one_smul'`, `support_smul_subset_vadd_support`, `coeff_smul_left`, `coeff_smul_right`, `single_zero_smul_eq_smul`
`instSMulZeroClass` 📖	CompOp	—
`instZero` 📖	CompOp	6 math math: `of_symm_smul`, `zero_smul'`, `of_smul`, `of_symm_zero`, `of_zero`, `single_zero_smul_eq_smul`
`of` 📖	CompOp	27 math math: `support_smul_subset_vadd_support'`, `coeff_single_smul_vadd`, `VertexOperator.of_coeff_apply_coeff`, `HVertexOperator.coeff_isPWOsupport`, `HahnSeries.SummableFamily.hsum_smul_module`, `HahnSeries.SummableFamily.smul_apply`, `HahnSeries.SummableFamily.smul_hsum`, `HahnSeries.of_symm_smul_of_eq_mul`, `HahnSeries.SummableFamily.smul_toFun`, `coeff_smul_order_add_order`, `of_symm_smul`, `ext_iff`, `of_symm_add`, `coeff_smul`, `coeff_single_zero_smul`, `orderTop_vAdd_le_orderTop_smul`, `of_smul`, `of_sub`, `of_add`, `support_smul_subset_vadd_support`, `of_symm_zero`, `of_zero`, `HVertexOperator.coeff_apply_apply`, `HVertexOperator.of_coeff_apply`, `coeff_smul_left`, `HVertexOperator.comp_apply`, `of_symm_sub`
`rec` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`SMulCommClass` 📖	mathematical	—	`SMulCommClass` `HahnSeries` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `HahnModule` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `instBaseSMul` `instSMul` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction`	—	`single_zero_smul_eq_smul` `mul_comm`
`add_smul` 📖	mathematical	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SMulWithZero.toSMulZeroClass` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`HahnSeries` `HahnModule` `instSMul` `HahnSeries.instAdd` `instAddCommMonoid`	—	`ext` `Set.IsPWO.union` `HahnSeries.isPWO_support` `coeff_smul_left` `Mathlib.Tactic.Contrapose.contrapose₂` `add_zero` `HahnSeries.coeff_add'` `of_symm_add` `Finset.sum_congr` `Set.subset_union_right` `Set.subset_union_left` `Finset.sum_add_distrib`
`coeff_single_smul_vadd` 📖	mathematical	—	`HahnSeries.coeff` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `Equiv` `HahnModule` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toZero` `HahnSeries` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `of` `instSMul` `ZeroHom` `HahnSeries.instZero` `ZeroHom.funLike` `HahnSeries.single` `HVAdd.hVAdd` `instHVAdd`	—	`map_zero` `ZeroHom.zeroHomClass` `HahnSeries.isPWO_support` `HahnSeries.support_zero` `Finset.sum_congr` `Finset.VAddAntidiagonal.congr_simp` `zero_smul` `Finset.sum_const_zero` `HahnSeries.support_single_of_ne` `smul_zero` `Finset.ext` `IsCancelVAdd.left_cancel` `instIsCancelVAddOfIsOrderedCancelVAdd` `Finset.sum_empty` `Finset.sum_singleton` `HahnSeries.coeff_single_same`
`coeff_single_zero_smul` 📖	mathematical	—	`HahnSeries.coeff` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `Equiv` `HahnModule` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toZero` `HahnSeries` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `of` `instSMul` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `ZeroHom` `HahnSeries.instZero` `ZeroHom.funLike` `HahnSeries.single`	—	`zero_vadd` `coeff_single_smul_vadd`
`coeff_smul` 📖	mathematical	—	`HahnSeries.coeff` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `Equiv` `HahnModule` `HahnSeries` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `of` `instSMul` `Finset.sum` `Finset.VAddAntidiagonal` `HahnSeries.support` `HahnSeries.isPWO_support`	—	—
`coeff_smul_left` 📖	mathematical	`Set.IsPWO` `PartialOrder.toPreorder` `Set` `Set.instHasSubset` `HahnSeries.support`	`HahnSeries.coeff` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `Equiv` `HahnModule` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `HahnSeries` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `of` `instSMul` `Finset.sum` `Finset.VAddAntidiagonal` `HahnSeries.isPWO_support`	—	`HahnSeries.isPWO_support` `coeff_smul` `Finset.sum_subset_zero_on_sdiff` `Finset.vaddAntidiagonal_mono_left` `zero_smul`
`coeff_smul_order_add_order` 📖	mathematical	—	`HahnSeries.coeff` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `Equiv` `HahnModule` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `HahnSeries` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `of` `instSMul` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `HahnSeries.order` `HahnSeries.leadingCoeff`	—	`instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid` `zero_smul'` `HahnSeries.order_zero` `zero_add` `HahnSeries.leadingCoeff_zero` `zero_smul` `add_zero` `HahnSeries.isPWO_support` `HahnSeries.support_zero` `Finset.sum_congr` `Finset.VAddAntidiagonal.congr_simp` `smul_zero` `Finset.sum_const_zero` `HahnSeries.isWF_support` `HahnSeries.support_nonempty_iff` `HahnSeries.order_of_ne` `coeff_smul` `HahnSeries.orderTop_ne_top` `HahnSeries.leadingCoeff_of_ne_zero` `vadd_eq_add` `Set.IsWF.isPWO` `Finset.vaddAntidiagonal_min_vadd_min` `Finset.sum_singleton` `WithTop.untop.congr_simp`
`coeff_smul_right` 📖	mathematical	`Set.IsPWO` `PartialOrder.toPreorder` `Set` `Set.instHasSubset` `HahnSeries.support` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `Equiv` `HahnModule` `SMulZeroClass.toSMul` `HahnSeries` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `of`	`HahnSeries.coeff` `instSMul` `Finset.sum` `Finset.VAddAntidiagonal` `HahnSeries.isPWO_support`	—	`HahnSeries.isPWO_support` `coeff_smul` `Finset.sum_subset_zero_on_sdiff` `Finset.vaddAntidiagonal_mono_right` `smul_zero`
`ext` 📖	—	`HahnSeries.coeff` `DFunLike.coe` `Equiv` `HahnModule` `HahnSeries` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `of`	—	—	`Equiv.injective`
`ext_iff` 📖	mathematical	—	`HahnSeries.coeff` `DFunLike.coe` `Equiv` `HahnModule` `HahnSeries` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `of`	—	`ext`
`instIsScalarTowerHahnSeries` 📖	mathematical	—	`IsScalarTower` `HahnSeries` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `HahnSeries.instSMul` `SMulWithZero.toSMulZeroClass`	—	`HahnSeries.ext` `smul_assoc`
`instIsScalarTowerHahnSeries_1` 📖	mathematical	—	`IsScalarTower` `HahnSeries` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `HahnModule` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `HahnSeries.instSMul` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `NonUnitalNonAssocSemiring.toDistribSMul` `instSMul` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `instBaseSMul`	—	`HahnSeries.single_zero_mul_eq_smul` `single_zero_smul_eq_smul`
`instIsTorsionFree` 📖	mathematical	—	`Module.IsTorsionFree` `HahnSeries` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `HahnModule` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `HahnSeries.instSemiring` `instAddCommMonoid` `instModule` `AddMonoid.toAddAction` `AddCommMonoid.toAddMonoid` `instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid`	—	`Module.IsTorsionFree.of_smul_eq_zero` `instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid` `HahnSeries.instNontrivialOfNonempty` `Zero.instNonempty` `IsDomain.toNontrivial` `Mathlib.Tactic.Contrapose.contrapose₁` `ext_iff` `coeff_smul_order_add_order` `IsDomain.toIsCancelMulZero`
`of_add` 📖	mathematical	—	`DFunLike.coe` `Equiv` `HahnSeries` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `HahnModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `HahnSeries.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoid`	—	—
`of_smul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `HahnSeries` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `HahnModule` `SMulZeroClass.toSMul` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `HahnSeries.instSMul` `instZero` `instBaseSMulZeroClass`	—	—
`of_sub` 📖	mathematical	—	`DFunLike.coe` `Equiv` `HahnSeries` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `HahnModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `HahnSeries.instSub` `AddCommGroup.toAddGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `instAddCommGroup`	—	—
`of_symm_add` 📖	mathematical	—	`DFunLike.coe` `Equiv` `HahnModule` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `HahnSeries` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `of` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoid` `HahnSeries.instAdd`	—	—
`of_symm_smul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `HahnModule` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SMulZeroClass.toSMul` `HahnSeries` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `of` `instZero` `instBaseSMulZeroClass` `HahnSeries.instSMul`	—	—
`of_symm_sub` 📖	mathematical	—	`DFunLike.coe` `Equiv` `HahnModule` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `HahnSeries` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `of` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instAddCommGroup` `HahnSeries.instSub`	—	—
`of_symm_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv` `HahnModule` `HahnSeries` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `of` `instZero` `HahnSeries.instZero`	—	—
`of_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv` `HahnSeries` `HahnModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `HahnSeries.instZero` `instZero`	—	—
`one_smul'` 📖	mathematical	—	`HahnSeries` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `HahnModule` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `MulActionWithZero.toSMulWithZero` `instSMul` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `HahnSeries.instOne` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	—	`ext` `coeff_single_zero_smul` `one_smul`
`orderTop_vAdd_le_orderTop_smul` 📖	mathematical	`WithTop.some` `HVAdd.hVAdd` `instHVAdd` `WithTop`	`Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `HahnSeries.orderTop` `MulZeroClass.toZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `Equiv` `HahnModule` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `HahnSeries` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `of` `instSMul`	—	`HahnSeries.orderTop_zero` `zero_smul'` `smul_zero` `HahnSeries.isWF_support` `HahnSeries.support_nonempty_iff` `HahnSeries.orderTop_of_ne_zero` `Set.IsWF.vadd` `IsOrderedCancelVAdd.toIsOrderedVAdd` `Set.Nonempty.vadd` `Set.IsWF.min_vadd` `OrderTop.le_top` `WithTop.coe_le_coe` `Set.IsWF.min_le_min_of_subset` `support_smul_subset_vadd_support`
`single_zero_smul_eq_smul` 📖	mathematical	—	`HahnSeries` `MulZeroClass.toZero` `HahnModule` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `instSMul` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `DFunLike.coe` `ZeroHom` `HahnSeries.instZero` `ZeroHom.funLike` `HahnSeries.single` `instZero` `instBaseSMulZeroClass`	—	`ext` `coeff_single_zero_smul`
`smul_add` 📖	mathematical	—	`HahnSeries` `HahnModule` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `instSMul` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoid`	—	`ext` `Set.IsPWO.union` `HahnSeries.isPWO_support` `coeff_smul_right` `Mathlib.Tactic.Contrapose.contrapose₂` `add_zero` `of_symm_add` `Finset.sum_congr` `Set.subset_union_right` `Set.subset_union_left` `smul_add` `Finset.sum_add_distrib`
`support_smul_subset_vadd_support` 📖	mathematical	—	`Set` `Set.instHasSubset` `HahnSeries.support` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `Equiv` `HahnModule` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toZero` `HahnSeries` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `of` `instSMul` `HVAdd.hVAdd` `instHVAdd` `Set.vadd`	—	`support_smul_subset_vadd_support'`
`support_smul_subset_vadd_support'` 📖	mathematical	—	`Set` `Set.instHasSubset` `HahnSeries.support` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `Equiv` `HahnModule` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toZero` `HahnSeries` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `of` `instSMul` `HVAdd.hVAdd` `instHVAdd` `Set.vadd`	—	`Set.Subset.trans` `HahnSeries.isPWO_support` `Mathlib.Tactic.Contrapose.contrapose₁` `Finset.sum_congr` `Finset.support_vaddAntidiagonal_subset_vadd`
`zero_smul'` 📖	mathematical	—	`HahnSeries` `HahnModule` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `instSMul` `HahnSeries.instZero` `instZero`	—	`ext` `HahnSeries.isPWO_support` `HahnSeries.support_zero` `Finset.sum_congr` `Finset.VAddAntidiagonal.congr_simp` `zero_smul` `Finset.sum_const_zero`

HahnSeries

Definitions

Name	Category	Theorems
`C` 📖	CompOp	14 math math: `C_injective`, `LaurentSeries.algebraMap_C_mem_adicCompletionIntegers`, `map_C`, `LaurentSeries.algebraMap_apply`, `embDomainRingHom_C`, `algebraMap_apply`, `C_eq_algebraMap`, `C_zero`, `PowerSeries.coe_C`, `C_mul_eq_smul`, `C_one`, `order_C`, `C_apply`, `ofPowerSeries_C`
`embDomainAlgHom` 📖	CompOp	1 math math: `embDomainAlgHom_apply_coeff`
`embDomainRingHom` 📖	CompOp	2 math math: `embDomainRingHom_apply`, `embDomainRingHom_C`
`instAddCommGroupWithOne` 📖	CompOp	—
`instAddCommMonoidWithOne` 📖	CompOp	—
`instAlgebra` 📖	CompOp	14 math math: `PowerSeries.heval_C`, `PowerSeries.coeff_heval`, `instNontrivialSubalgebra`, `PowerSeries.heval_apply`, `algebraMap_apply`, `C_eq_algebraMap`, `embDomainAlgHom_apply_coeff`, `toPowerSeriesAlg_apply`, `toPowerSeriesAlg_symm_apply_coeff`, `ofPowerSeriesAlg_apply_coeff`, `PowerSeries.heval_X`, `PowerSeries.heval_unit`, `PowerSeries.coeff_heval_zero`, `PowerSeries.heval_mul`
`instCommRing` 📖	CompOp	2 math math: `LaurentSeries.powerSeriesEquivSubring_apply`, `LaurentSeries.powerSeriesEquivSubring_coe_apply`
`instCommSemiring` 📖	CompOp	2 math math: `LaurentSeries.of_powerSeries_localization`, `LaurentSeries.instIsFractionRingPowerSeries`
`instDistrib` 📖	CompOp	—
`instIntCast` 📖	CompOp	1 math math: `single_zero_intCast`
`instMul` 📖	CompOp	62 math math: `instNoZeroDivisorsFinsuppNat`, `SummableFamily.mul_toFun`, `leadingCoeff_mul`, `LaurentSeries.LaurentSeriesRingEquiv_def`, `coeff_single_mul_add`, `coeff_mul`, `LaurentSeries.ofPowerSeries_powerSeriesPart`, `LaurentSeries.single_order_mul_powerSeriesPart`, `single_mul_single`, `single_zero_mul_eq_smul`, `order_mul`, `coeff_mul_left'`, `toMvPowerSeries_symm_apply_coeff`, `instIsCancelMulZeroOfIsCancelAdd`, `orderTop_mul_of_nonzero`, `one_minus_single_neg_mul`, `PowerSeries.coe_mul`, `order_single_mul_of_isRegular`, `coeff_single_zero_mul`, `map_mul`, `of_symm_smul_of_eq_mul`, `order_mul_of_nonzero`, `instNoZeroDivisors`, `leadingCoeff_mul_of_ne_zero`, `coeff_mul_order_add_order`, `orderTop_mul_of_ne_zero`, `unit_aux`, `LaurentSeries.coe_X_compare`, `cardSupp_mul_single_le`, `cardSupp_single_mul_le`, `LaurentSeries.exists_powerSeries_of_memIntegers`, `orderTop_mul`, `coeff_toPowerSeries`, `LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring`, `coeff_toPowerSeries_symm`, `LaurentSeries.powerSeriesRingEquiv_coe_apply`, `orderTop_add_le_mul`, `SummableFamily.one_sub_self_mul_hsum_powers`, `support_mul_subset_add_support`, `coeff_toMvPowerSeries_symm`, `embDomain_mul`, `inv_def`, `coeff_mul_right'`, `C_mul_eq_smul`, `coeff_toMvPowerSeries`, `coeff_mul_single`, `SummableFamily.hsum_smul`, `SummableFamily.hsum_mul`, `support_mul_subset`, `leadingCoeff_mul_of_nonzero`, `ofPowerSeries_apply`, `toMvPowerSeries_apply`, `LaurentSeries.ratfuncAdicComplRingEquiv_apply`, `coeff_mul_single_add`, `coeff_mul_single_zero`, `order_mul_of_ne_zero`, `LaurentSeries.mem_integers_of_powerSeries`, `toPowerSeries_apply`, `PowerSeries.heval_mul`, `toPowerSeries_symm_apply_coeff`, `coeff_single_mul`, `cardSupp_mul_le`
`instNNRatCast` 📖	CompOp	2 math math: `single_zero_ofScientific`, `single_zero_nnratCast`
`instNatCast` 📖	CompOp	1 math math: `single_zero_natCast`
`instNonAssocRing` 📖	CompOp	—
`instNonAssocSemiring` 📖	CompOp	50 math math: `C_injective`, `LaurentSeries.LaurentSeriesRingEquiv_def`, `ofPowerSeries_X_pow`, `PowerSeries.coe_add`, `SummableFamily.lsum_apply`, `LaurentSeries.ofPowerSeries_powerSeriesPart`, `LaurentSeries.single_order_mul_powerSeriesPart`, `embDomainRingHom_apply`, `PowerSeries.coeff_coe`, `LaurentSeries.coe_algebraMap`, `RatFunc.coe_coe`, `PowerSeries.coe_smul`, `LaurentSeries.algebraMap_C_mem_adicCompletionIntegers`, `map_C`, `LaurentSeries.val_le_one_iff_eq_coe`, `PowerSeries.coe_mul`, `PowerSeries.coe_sub`, `LaurentSeries.algebraMap_apply`, `embDomainRingHom_C`, `algebraMap_apply`, `ofPowerSeries_apply_coeff`, `ofPowerSeries_X`, `LaurentSeries.coe_X_compare`, `LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero`, `C_zero`, `PowerSeries.coe_zero`, `LaurentSeries.exists_powerSeries_of_memIntegers`, `PowerSeries.coe_C`, `PowerSeries.coe_neg`, `LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring`, `LaurentSeries.powerSeries_ext_subring`, `LaurentSeries.powerSeriesRingEquiv_coe_apply`, `LaurentSeries.powerSeriesEquivSubring_apply`, `Polynomial.algebraMap_hahnSeries_apply`, `LaurentSeries.powerSeriesEquivSubring_coe_apply`, `PowerSeries.coe_X`, `C_mul_eq_smul`, `C_one`, `order_C`, `ofPowerSeries_apply`, `PowerSeries.coe_one`, `ofPowerSeries_injective`, `C_apply`, `ofPowerSeries_C`, `PowerSeries.coe_pow`, `LaurentSeries.mem_integers_of_powerSeries`, `algebraMap_apply'`, `LaurentSeries.X_order_mul_powerSeriesPart`, `LaurentSeries.coeff_coe_powerSeries`, `LaurentSeries.valuation_X_pow`
`instNonUnitalCommRing` 📖	CompOp	—
`instNonUnitalCommSemiring` 📖	CompOp	—
`instNonUnitalNonAssocRing` 📖	CompOp	—
`instNonUnitalNonAssocSemiring` 📖	CompOp	—
`instNonUnitalRing` 📖	CompOp	—
`instNonUnitalSemiring` 📖	CompOp	—
`instOne` 📖	CompOp	26 math math: `PowerSeries.heval_C`, `SummableFamily.powers_zero`, `orderTop_sub_pos`, `SummableFamily.powers_of_not_orderTop_pos`, `orderTop_one`, `cardSupp_one_le`, `one_minus_single_neg_mul`, `embDomain_one`, `SummableFamily.embDomain_succ_smul_powers`, `map_one`, `SummableFamily.powerSeriesFamily_hsum_zero`, `unit_aux`, `coeff_one`, `single_zero_one`, `SummableFamily.one_sub_self_mul_hsum_powers`, `inv_def`, `leadingCoeff_one`, `HahnModule.one_smul'`, `orderTop_self_sub_one_pos_iff`, `C_one`, `order_one`, `PowerSeries.coe_one`, `coeff_toOrderTopSubOnePos_pow`, `mem_orderTopSubOnePos_iff`, `support_one`, `cardSupp_one`
`instRatCast` 📖	CompOp	1 math math: `single_zero_ratCast`
`instRing` 📖	CompOp	25 math math: `LaurentSeries.valuation_le_iff_coeff_lt_eq_zero`, `LaurentSeries.valuation_single_zpow`, `LaurentSeries.inducing_coe`, `LaurentSeries.continuous_coe`, `LaurentSeries.val_le_one_iff_eq_coe`, `mem_cardSuppLTSubring`, `addVal_le_of_coeff_ne_zero`, `LaurentSeries.exists_ratFunc_val_lt`, `LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero`, `addVal_apply_of_ne`, `LaurentSeries.valuation_LaurentSeries_equal_extension`, `LaurentSeries.powerSeries_ext_subring`, `LaurentSeries.powerSeriesEquivSubring_apply`, `LaurentSeries.powerSeriesEquivSubring_coe_apply`, `LaurentSeries.instLaurentSeriesComplete`, `LaurentSeries.valuation_coe_ratFunc`, `LaurentSeries.valuation_compare`, `LaurentSeries.coe_range_dense`, `LaurentSeries.comparePkg_eq_extension`, `LaurentSeries.valuation_def`, `LaurentSeries.valuation_le_iff_coeff_lt_log_eq_zero`, `LaurentSeries.uniformContinuous_coeff`, `addVal_apply`, `LaurentSeries.exists_ratFunc_eq_v`, `LaurentSeries.valuation_X_pow`
`instSemiring` 📖	CompOp	60 math math: `RatFunc.instFaithfulSMulPolynomialLaurentSeries`, `PowerSeries.heval_C`, `instIsStrictOrderedRingLexOfIsDomain`, `single_pow`, `PowerSeries.coeff_heval`, `SummableFamily.binomialFamily_apply_of_orderTop_nonpos`, `SummableFamily.lsum_apply`, `RatFunc.coe_X`, `LaurentSeries.coe_algebraMap`, `RatFunc.coe_coe`, `LaurentSeries.inducing_coe`, `LaurentSeries.continuous_coe`, `SummableFamily.coe_powers`, `SummableFamily.co_support_zero`, `isUnit_of_isUnit_leadingCoeff_AddUnitOrder`, `instNontrivialSubalgebra`, `PowerSeries.heval_apply`, `LaurentSeries.algebraMap_apply`, `LaurentSeries.exists_ratFunc_val_lt`, `SummableFamily.support_pow_subset_closure`, `algebraMap_apply`, `C_eq_algebraMap`, `embDomainAlgHom_apply_coeff`, `RatFunc.valuation_eq_LaurentSeries_valuation`, `RatFunc.algebraMap_apply_div`, `toPowerSeriesAlg_apply`, `isUnit_iff`, `toPowerSeriesAlg_symm_apply_coeff`, `binomial_power`, `SummableFamily.isPWO_iUnion_support_powers`, `pow_add`, `orderTop_nsmul_le_orderTop_pow`, `LaurentSeries.LaurentSeries_coe`, `ofPowerSeriesAlg_apply_coeff`, `PowerSeries.heval_X`, `SummableFamily.binomialFamily_apply`, `Polynomial.algebraMap_hahnSeries_apply`, `Polynomial.algebraMap_hahnSeries_injective`, `LaurentSeries.valuation_coe_ratFunc`, `SummableFamily.powerSeriesFamily_of_orderTop_pos`, `RatFunc.single_one_eq_pow`, `SummableFamily.powers_toFun`, `PowerSeries.heval_unit`, `LaurentSeries.coe_range_dense`, `order_pow`, `isUnit_of_orderTop_pos`, `instIsOrderedRingLexOfNoZeroDivisors`, `coeff_toOrderTopSubOnePos_pow`, `PowerSeries.coeff_heval_zero`, `instIsDomainOfIsCancelAdd`, `SummableFamily.powers_of_orderTop_pos`, `HahnModule.instIsTorsionFree`, `PowerSeries.coe_pow`, `PowerSeries.heval_mul`, `algebraMap_apply'`, `val_toOrderTopSubOnePos_coe`, `mem_orderTopSubOnePos_iff`, `val_inv_toOrderTopSubOnePos_coe`, `LaurentSeries.valuation_X_pow`, `cardSupp_pow_le`
`orderTopSubOnePos` 📖	CompOp	6 math math: `binomial_power`, `pow_add`, `coeff_toOrderTopSubOnePos_pow`, `val_toOrderTopSubOnePos_coe`, `mem_orderTopSubOnePos_iff`, `val_inv_toOrderTopSubOnePos_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`C_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `HahnSeries` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instNonAssocSemiring` `RingHom.instFunLike` `C` `ZeroHom` `instZero` `ZeroHom.funLike` `single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`C_eq_algebraMap` 📖	mathematical	—	`C` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `algebraMap` `HahnSeries` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instSemiring` `instAlgebra` `Algebra.id`	—	—
`C_injective` 📖	mathematical	—	`HahnSeries` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `DFunLike.coe` `RingHom` `instNonAssocSemiring` `RingHom.instFunLike` `C`	—	`ext_iff` `coeff_single_same` `C_apply`
`C_mul_eq_smul` 📖	mathematical	—	`HahnSeries` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instMul` `DFunLike.coe` `RingHom` `instNonAssocSemiring` `RingHom.instFunLike` `C` `instSMul` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `NonUnitalNonAssocSemiring.toDistribSMul`	—	`single_zero_mul_eq_smul`
`C_ne_zero` 📖	—	—	—	—	`C_injective` `C_zero`
`C_one` 📖	mathematical	—	`DFunLike.coe` `RingHom` `HahnSeries` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instNonAssocSemiring` `RingHom.instFunLike` `C` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `instOne` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`RingHom.map_one`
`C_zero` 📖	mathematical	—	`DFunLike.coe` `RingHom` `HahnSeries` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instNonAssocSemiring` `RingHom.instFunLike` `C` `instZero`	—	`RingHom.map_zero`
`algebraMap_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `HahnSeries` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra` `instNonAssocSemiring` `C`	—	—
`coeff_mul` 📖	mathematical	—	`coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `HahnSeries` `instMul` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.addAntidiagonal` `support` `isPWO_support` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`coeff_mul_left'` 📖	mathematical	`Set.IsPWO` `PartialOrder.toPreorder` `Set` `Set.instHasSubset` `support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`coeff` `HahnSeries` `instMul` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.addAntidiagonal` `isPWO_support` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`HahnModule.coeff_smul_left` `instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid`
`coeff_mul_order_add_order` 📖	mathematical	—	`coeff` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `HahnSeries` `instMul` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `order` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `leadingCoeff`	—	`HahnModule.coeff_smul_order_add_order`
`coeff_mul_right'` 📖	mathematical	`Set.IsPWO` `PartialOrder.toPreorder` `Set` `Set.instHasSubset` `support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`coeff` `HahnSeries` `instMul` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.addAntidiagonal` `isPWO_support` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`HahnModule.coeff_smul_right` `instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid`
`coeff_mul_single` 📖	mathematical	—	`coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `HahnSeries` `instMul` `AddCommGroup.toAddCommMonoid` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `DFunLike.coe` `ZeroHom` `instZero` `ZeroHom.funLike` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `sub_add_cancel` `coeff_mul_single_add`
`coeff_mul_single_add` 📖	mathematical	—	`coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `HahnSeries` `instMul` `DFunLike.coe` `ZeroHom` `instZero` `ZeroHom.funLike` `single` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`map_zero` `ZeroHom.zeroHomClass` `isPWO_support` `support_zero` `Finset.sum_congr` `Finset.addAntidiagonal.congr_simp` `MulZeroClass.mul_zero` `Finset.sum_const_zero` `support_single_of_ne` `MulZeroClass.zero_mul` `Finset.ext` `add_right_cancel` `IsCancelAdd.toIsRightCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `Finset.sum_empty` `Finset.sum_singleton` `coeff_single_same`
`coeff_mul_single_zero` 📖	mathematical	—	`coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `HahnSeries` `instMul` `DFunLike.coe` `ZeroHom` `instZero` `ZeroHom.funLike` `single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`add_zero` `coeff_mul_single_add`
`coeff_one` 📖	mathematical	—	`coeff` `HahnSeries` `instOne`	—	`coeff_single`
`coeff_single_mul` 📖	mathematical	—	`coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `HahnSeries` `instMul` `AddCommGroup.toAddCommMonoid` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `DFunLike.coe` `ZeroHom` `instZero` `ZeroHom.funLike` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `sub_add_cancel` `coeff_single_mul_add`
`coeff_single_mul_add` 📖	mathematical	—	`coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `HahnSeries` `instMul` `DFunLike.coe` `ZeroHom` `instZero` `ZeroHom.funLike` `single` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid` `of_symm_smul_of_eq_mul` `add_comm` `vadd_eq_add` `HahnModule.coeff_single_smul_vadd`
`coeff_single_zero_mul` 📖	mathematical	—	`coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `HahnSeries` `instMul` `DFunLike.coe` `ZeroHom` `instZero` `ZeroHom.funLike` `single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`add_zero` `coeff_single_mul_add`
`embDomainAlgHom_apply_coeff` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `Preorder.toLE` `PartialOrder.toPreorder`	`coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AlgHom` `HahnSeries` `instSemiring` `instAlgebra` `AlgHom.funLike` `embDomainAlgHom` `Set` `Set.instMembership` `Set.image` `support`	—	—
`embDomainRingHom_C` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `Preorder.toLE` `PartialOrder.toPreorder`	`RingHom` `HahnSeries` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instNonAssocSemiring` `RingHom.instFunLike` `embDomainRingHom` `C`	—	`embDomain_single` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass`
`embDomainRingHom_apply` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `Preorder.toLE` `PartialOrder.toPreorder`	`RingHom` `HahnSeries` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instNonAssocSemiring` `RingHom.instFunLike` `embDomainRingHom` `embDomain`	—	—
`embDomain_mul` 📖	mathematical	`DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `instFunLikeOrderEmbedding` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`embDomain` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `HahnSeries` `instMul`	—	`ext` `isPWO_support` `embDomain_coeff` `Finset.sum_map` `Finset.sum_congr` `Finset.sum_subset` `Finset.addAntidiagonal.congr_simp` `Mathlib.Tactic.Contrapose.contrapose₂` `support_embDomain_subset` `ne_zero_and_ne_zero_of_mul` `embDomain_notin_range` `support_mul_subset` `mem_support`
`embDomain_one` 📖	mathematical	`DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `instFunLikeOrderEmbedding` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`embDomain` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `HahnSeries` `instOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`embDomain_single`
`instIsCancelMulZeroOfIsCancelAdd` 📖	mathematical	—	`IsCancelMulZero` `HahnSeries` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instMul` `instZero`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Set.IsWF.mono` `Set.IsWF.union` `isWF_support` `Set.IsWF.min_mem` `isPWO_support` `coeff_mul` `Finset.sum_subset` `Finset.subset_union_left` `MulZeroClass.mul_zero` `Finset.subset_union_right` `Finset.sum_eq_sum_iff_single` `AddRightCancelSemigroup.toIsRightCancelAdd` `IsCancelAdd.toIsLeftCancelAdd` `IsCancelMulZero.toIsLeftCancelMulZero` `add_eq_add_iff_eq_and_eq` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `IsCancelAdd.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `order_le_of_coeff_ne_zero` `Set.IsWF.min_le` `mul_right_inj'` `Iff.not` `coeff_order_eq_zero` `MulZeroClass.zero_mul` `IsCancelMulZero.toIsRightCancelMulZero` `mul_left_inj'`
`instIsDomainOfIsCancelAdd` 📖	mathematical	—	`IsDomain` `HahnSeries` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring`	—	`instIsCancelMulZeroOfIsCancelAdd` `IsDomain.toIsCancelMulZero` `instNontrivialOfNonempty` `Zero.instNonempty` `IsDomain.toNontrivial`
`instNoZeroDivisors` 📖	mathematical	—	`NoZeroDivisors` `HahnSeries` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instMul` `instZero`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `coeff_mul_order_add_order`
`instNontrivialSubalgebra` 📖	mathematical	—	`Nontrivial` `Subalgebra` `HahnSeries` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSemiring` `instAlgebra` `Algebra.id`	—	`SetLike.ext_iff` `exists_ne` `ext_iff` `coeff_single_same` `algebraMap_apply` `C_apply` `coeff_single_of_ne` `zero_ne_one` `NeZero.one`
`leadingCoeff_mul` 📖	mathematical	—	`leadingCoeff` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `HahnSeries` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`MulZeroClass.zero_mul` `leadingCoeff_zero` `MulZeroClass.mul_zero` `leadingCoeff_mul_of_ne_zero`
`leadingCoeff_mul_of_ne_zero` 📖	mathematical	—	`leadingCoeff` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `HahnSeries` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`leadingCoeff_eq` `order_mul_of_ne_zero` `coeff_mul_order_add_order`
`leadingCoeff_mul_of_nonzero` 📖	mathematical	—	`leadingCoeff` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `HahnSeries` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`leadingCoeff_mul_of_ne_zero`
`leadingCoeff_one` 📖	mathematical	—	`leadingCoeff` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `HahnSeries` `instOne` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	—	`leadingCoeff_eq` `order_one` `coeff_one`
`map_C` 📖	mathematical	—	`map` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `DFunLike.coe` `RingHom` `HahnSeries` `instNonAssocSemiring` `RingHom.instFunLike` `C` `MonoidWithZeroHomClass.toZeroHomClass` `NonAssocSemiring.toMulZeroOneClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`	—	`ext` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `coeff_single_same` `coeff_single_of_ne` `map_zero`
`map_mul` 📖	mathematical	—	`map` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `HahnSeries` `instMul` `NonUnitalRingHom` `NonUnitalRingHom.instFunLike` `AddMonoidHomClass.toZeroHomClass` `NonUnitalRingHomClass.toAddMonoidHomClass` `NonUnitalRingHom.instNonUnitalRingHomClass`	—	`ext` `AddMonoidHomClass.toZeroHomClass` `NonUnitalRingHomClass.toAddMonoidHomClass` `NonUnitalRingHom.instNonUnitalRingHomClass` `isPWO_support` `map_sum` `Finset.sum_congr` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `Finset.sum_subset` `map_zero` `mul_eq_zero_of_left` `mul_eq_zero_of_right`
`map_one` 📖	mathematical	—	`map` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `HahnSeries` `instOne` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZeroHom` `MonoidWithZeroHom.funLike` `MonoidWithZeroHomClass.toZeroHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass`	—	`ZeroHom.zeroHomClass` `map_single` `MonoidWithZeroHom.map_one`
`mem_orderTopSubOnePos_iff` 📖	mathematical	—	`Units` `HahnSeries` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `orderTopSubOnePos` `WithTop` `Preorder.toLT` `WithTop.instPreorder` `PartialOrder.toPreorder` `WithTop.zero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `orderTop` `instSub` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `Units.val` `instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	—
`of_symm_smul_of_eq_mul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `HahnModule` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `NonUnitalNonAssocSemiring.toDistribSMul` `HahnSeries` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `HahnModule.of` `HahnModule.instSMul` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid` `instMul`	—	`instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid`
`orderTop_add_le_mul` 📖	mathematical	—	`WithTop` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `WithTop.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `orderTop` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `HahnSeries` `instMul`	—	`smul_eq_mul` `HahnModule.orderTop_vAdd_le_orderTop_smul` `instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid`
`orderTop_mul` 📖	mathematical	—	`orderTop` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `HahnSeries` `instMul` `WithTop` `WithTop.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`MulZeroClass.zero_mul` `orderTop_zero` `MulZeroClass.mul_zero` `WithTop.add_top` `orderTop_mul_of_ne_zero`
`orderTop_mul_of_ne_zero` 📖	mathematical	—	`orderTop` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `HahnSeries` `instMul` `WithTop` `WithTop.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`MulZeroClass.zero_mul` `orderTop_zero` `MulZeroClass.mul_zero` `WithTop.add_top` `coeff_mul_order_add_order` `order_eq_orderTop_of_ne_zero` `WithTop.coe_add` `WithTop.coe_eq_coe` `le_antisymm` `order_le_of_coeff_ne_zero` `isWF_support` `support_nonempty_iff` `order_of_ne` `Set.IsWF.add` `Set.Nonempty.add` `Set.IsWF.min_add` `Set.IsWF.min_le_min_of_subset` `support_mul_subset`
`orderTop_mul_of_nonzero` 📖	mathematical	—	`orderTop` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `HahnSeries` `instMul` `WithTop` `WithTop.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`orderTop_mul_of_ne_zero`
`orderTop_nsmul_le_orderTop_pow` 📖	mathematical	—	`WithTop` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoid.toNatSMul` `WithTop.addMonoid` `AddCommMonoid.toAddMonoid` `orderTop` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `HahnSeries` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring`	—	`zero_smul` `pow_zero` `orderTop_one` `not_nontrivial_iff_subsingleton` `NeZero.one` `orderTop_of_subsingleton` `add_nsmul` `pow_add` `add_le_add_left` `WithTop.addRightMono` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `one_nsmul` `orderTop_add_le_mul` `pow_one` `le_refl`
`orderTop_one` 📖	mathematical	—	`orderTop` `HahnSeries` `instOne` `WithTop` `WithTop.zero`	—	`single_zero_one` `orderTop_single` `one_ne_zero` `WithTop.coe_eq_zero`
`orderTop_self_sub_one_pos_iff` 📖	mathematical	—	`WithTop` `Preorder.toLT` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `WithTop.zero` `orderTop` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `HahnSeries` `instSub` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `leadingCoeff`	—	`sub_add_cancel` `add_comm` `orderTop_one` `NeZero.one` `orderTop_add_eq_left` `leadingCoeff_one` `leadingCoeff_add_eq_left` `lt_of_le_of_ne` `min_self` `min_orderTop_le_orderTop_sub` `orderTop_sub_ne`
`orderTop_sub_pos` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder`	`WithTop` `WithTop.instPreorder` `WithTop.zero` `orderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `HahnSeries` `instSub` `AddCommGroup.toAddGroup` `instAdd` `SubNegMonoid.toAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `instOne` `DFunLike.coe` `ZeroHom` `instZero` `ZeroHom.funLike` `single`	—	`map_zero` `ZeroHom.zeroHomClass` `add_zero` `sub_self` `orderTop_zero` `add_sub_cancel_left` `orderTop_single`
`order_C` 📖	mathematical	—	`order` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `RingHom` `HahnSeries` `instNonAssocSemiring` `RingHom.instFunLike` `C`	—	`C_zero` `order_zero` `order_single`
`order_mul` 📖	mathematical	—	`order` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `HahnSeries` `instMul` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`le_antisymm` `order_le_of_coeff_ne_zero` `coeff_mul_order_add_order` `isWF_support` `support_nonempty_iff` `order_of_ne` `mul_ne_zero` `instNoZeroDivisors` `Set.IsWF.add` `Set.Nonempty.add` `Set.IsWF.min_add` `Set.IsWF.min_le_min_of_subset` `support_mul_subset`
`order_mul_of_ne_zero` 📖	mathematical	—	`order` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `HahnSeries` `instMul` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`leadingCoeff_zero` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `ne_of_eq_of_ne` `coeff_mul_order_add_order` `le_antisymm` `order_le_of_coeff_ne_zero` `isWF_support` `support_nonempty_iff` `leadingCoeff_ne_zero` `order_of_ne` `ne_zero_of_coeff_ne_zero` `Set.IsWF.add` `Set.Nonempty.add` `Set.IsWF.min_add` `Set.IsWF.min_le_min_of_subset` `support_mul_subset`
`order_mul_of_nonzero` 📖	mathematical	—	`order` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `HahnSeries` `instMul` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`order_mul_of_ne_zero`
`order_one` 📖	mathematical	—	`order` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `HahnSeries` `instOne` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass`	—	`subsingleton_or_nontrivial` `instSubsingleton` `order_zero` `order_single` `one_ne_zero` `NeZero.one`
`order_pow` 📖	mathematical	—	`order` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `HahnSeries` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `AddMonoid.toNatSMul`	—	`pow_zero` `order_one` `zero_nsmul` `eq_or_ne` `pow_succ` `MulZeroClass.mul_zero` `order_zero` `nsmul_zero` `order_mul` `isReduced_of_noZeroDivisors` `instNoZeroDivisors` `succ_nsmul`
`order_single_mul_of_isRegular` 📖	mathematical	`IsRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`order` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `HahnSeries` `instMul` `DFunLike.coe` `ZeroHom` `instZero` `ZeroHom.funLike` `single` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`subsingleton_or_nontrivial` `Subsingleton.eq_zero` `instSubsingleton` `leadingCoeff_of_single` `IsLeftRegular.mul_left_eq_zero_iff` `IsRegular.left` `leadingCoeff_eq_zero` `order_mul_of_ne_zero` `order_single` `IsRegular.ne_zero`
`single_mul_single` 📖	mathematical	—	`HahnSeries` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instMul` `DFunLike.coe` `ZeroHom` `instZero` `ZeroHom.funLike` `single` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`ext` `coeff_mul_single_add` `coeff_single_same` `coeff_single_of_ne` `isPWO_support` `coeff_mul` `Finset.sum_eq_zero` `eq_of_mem_support_single`
`single_pow` 📖	mathematical	—	`HahnSeries` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `DFunLike.coe` `ZeroHom` `instZero` `ZeroHom.funLike` `single` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid`	—	`ext` `pow_zero` `coeff_one` `zero_smul` `coeff_single` `pow_succ` `single_mul_single` `succ_nsmul`
`single_zero_intCast` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `HahnSeries` `instZero` `ZeroHom.funLike` `single` `instIntCast`	—	—
`single_zero_mul_eq_smul` 📖	mathematical	—	`HahnSeries` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instMul` `DFunLike.coe` `ZeroHom` `instZero` `ZeroHom.funLike` `single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instSMul` `DistribSMul.toSMulZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `NonUnitalNonAssocSemiring.toDistribSMul`	—	`ext` `coeff_single_zero_mul`
`single_zero_natCast` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `HahnSeries` `instZero` `ZeroHom.funLike` `single` `instNatCast`	—	—
`single_zero_nnratCast` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `HahnSeries` `instZero` `ZeroHom.funLike` `single` `NNRat.cast` `instNNRatCast`	—	—
`single_zero_ofNat` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `HahnSeries` `instZero` `ZeroHom.funLike` `single`	—	—
`single_zero_one` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `HahnSeries` `instZero` `ZeroHom.funLike` `single` `instOne`	—	—
`single_zero_ratCast` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `HahnSeries` `instZero` `ZeroHom.funLike` `single` `instRatCast`	—	—
`support_mul_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `HahnSeries` `instMul` `Set.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`instIsOrderedCancelVAddOfIsOrderedAddCancelMonoid` `of_symm_smul_of_eq_mul` `vadd_eq_add` `HahnModule.support_smul_subset_vadd_support`
`support_mul_subset_add_support` 📖	mathematical	—	`Set` `Set.instHasSubset` `support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `HahnSeries` `instMul` `Set.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`support_mul_subset`
`support_one` 📖	mathematical	—	`support` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `HahnSeries` `instOne` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `Set` `Set.instSingletonSet`	—	`support_single_of_ne` `one_ne_zero` `NeZero.one`

(root)

Definitions

Name	Category	Theorems
`HahnModule` 📖	CompOp	46 math math: `HahnModule.support_smul_subset_vadd_support'`, `HahnModule.smul_add`, `HahnModule.coeff_single_smul_vadd`, `VertexOperator.of_coeff_apply_coeff`, `HVertexOperator.coeff_isPWOsupport`, `HahnModule.add_smul`, `HahnSeries.SummableFamily.hsum_smul_module`, `HahnSeries.SummableFamily.smul_apply`, `HahnSeries.SummableFamily.smul_hsum`, `HahnSeries.of_symm_smul_of_eq_mul`, `HahnSeries.SummableFamily.smul_toFun`, `VertexOperator.ncoeff_apply`, `HahnModule.coeff_smul_order_add_order`, `HahnModule.of_symm_smul`, `HahnModule.instIsScalarTowerHahnSeries_1`, `HVertexOperator.of_coeff_coeff`, `HVertexOperator.coeff_inj_iff`, `HahnModule.SMulCommClass`, `HahnModule.ext_iff`, `HahnModule.of_symm_add`, `HVertexOperator.coeff_inj`, `HahnModule.coeff_smul`, `HahnModule.coeff_single_zero_smul`, `VertexOperator.ext_iff`, `HVertexOperator.ext_iff`, `HahnModule.orderTop_vAdd_le_orderTop_smul`, `HahnModule.zero_smul'`, `HahnModule.one_smul'`, `HahnModule.of_smul`, `HahnModule.of_sub`, `HahnModule.of_add`, `VertexOperator.ncoeff_of_coeff`, `HahnModule.support_smul_subset_vadd_support`, `HVertexOperator.compHahnSeries_coeff`, `HahnModule.of_symm_zero`, `HahnModule.of_zero`, `HVertexOperator.coeff_comp`, `HVertexOperator.coeff_apply_apply`, `HVertexOperator.of_coeff_apply`, `HahnModule.coeff_smul_left`, `HahnModule.instIsTorsionFree`, `VertexOperator.coeff_eq_ncoeff`, `HVertexOperator.comp_apply`, `HVertexOperator.coeff_of_coeff`, `HahnModule.single_zero_smul_eq_smul`, `HahnModule.of_symm_sub`

---

← Back to Index