HahnEmbedding

📁 Source: Mathlib/Algebra/Order/Module/HahnEmbedding.lean

Statistics

Metric	Count
Definitions `ArchimedeanStrata`, `baseDomain`, `instDecompositionFiniteArchimedeanClassSubtypeMemSubmoduleBaseDomainStratum'`, `stratum`, `stratum'`, `IsPartial`, `eval`, `evalCoeff`, `extend`, `extendFun`, `instInhabitedOfIsOrderedAddMonoid`, `sSup`, `sSupFun`, `toOrderAddMonoidHom`, `Seed`, `baseEmbedding`, `coeff`, `coeff'`, `hahnCoeff`, `toArchimedeanStrata`	20
Theorems `archimedeanClassMk_of_mem_stratum`, `archimedean_stratum`, `ball_sup_stratum_eq`, `disjoint_ball_stratum`, `iSupIndep_stratum`, `iSupIndep_stratum'`, `instNonempty`, `isInternal_stratum'`, `nontrivial_stratum`, `stratum_ne_bot`, `baseEmbedding_le`, `strictMono`, `truncLT_mem_range`, `apply_of_mem_stratum`, `archimedeanClassMk_eq_iff`, `archimedeanClassMk_le_of_eval_eq`, `baseEmbedding_le_extendFun`, `baseEmbedding_le_sSupFun`, `coeff_eq_of_mem`, `coeff_eq_zero_of_mem`, `coeff_ne_zero`, `evalCoeff_eq`, `evalCoeff_eq_zero`, `eval_eq_truncLT`, `eval_lt`, `eval_ne`, `eval_smul`, `eval_zero`, `exists_domain_eq_top`, `exists_isMax`, `exists_sub_mem_ball`, `extendFun_strictMono`, `isPartial_extendFun`, `isPartial_sSupFun`, `isWF_support_evalCoeff`, `le_sSupFun`, `lt_extend`, `mem_domain`, `orderTop_eq_archimedeanClassMk`, `orderTop_eq_finiteArchimedeanClassMk`, `orderTop_eq_iff`, `sSupFun_strictMono`, `toOrderAddMonoidHom_apply`, `toOrderAddMonoidHom_injective`, `truncLT_eval_mem_range_extendFun`, `truncLT_mem_range_extendFun`, `truncLT_mem_range_sSupFun`, `val_sub_ne_zero`, `baseEmbedding_pos`, `baseEmbedding_strictMono`, `coeff_baseEmbedding`, `domain_baseEmbedding`, `hahnCoeff_apply`, `isPartial_baseEmbedding`, `mem_domain_baseEmbedding`, `strictMono_coeff`, `truncLT_mem_range_baseEmbedding`, `hahnEmbedding_isOrderedModule`	58
Total	78

HahnEmbedding

Definitions

Name	Category	Theorems
`ArchimedeanStrata` 📖	CompData	1 math math: `ArchimedeanStrata.instNonempty`
`IsPartial` 📖	CompData	10 math math: `Partial.orderTop_eq_archimedeanClassMk`, `Partial.archimedeanClassMk_eq_iff`, `Partial.toOrderAddMonoidHom_apply`, `Seed.isPartial_baseEmbedding`, `Partial.orderTop_eq_iff`, `Partial.orderTop_eq_finiteArchimedeanClassMk`, `Partial.mem_domain`, `Partial.exists_domain_eq_top`, `Partial.exists_isMax`, `Partial.toOrderAddMonoidHom_injective`
`Seed` 📖	CompData	1 math math: `instNonemptySeedRatReal`

HahnEmbedding.ArchimedeanStrata

Definitions

Name	Category	Theorems
`baseDomain` 📖	CompOp	3 math math: `isInternal_stratum'`, `iSupIndep_stratum'`, `HahnEmbedding.Seed.domain_baseEmbedding`
`instDecompositionFiniteArchimedeanClassSubtypeMemSubmoduleBaseDomainStratum'` 📖	CompOp	—
`stratum` 📖	CompOp	6 math math: `HahnEmbedding.Seed.strictMono_coeff`, `ball_sup_stratum_eq`, `disjoint_ball_stratum`, `nontrivial_stratum`, `archimedean_stratum`, `iSupIndep_stratum`
`stratum'` 📖	CompOp	2 math math: `isInternal_stratum'`, `iSupIndep_stratum'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`archimedeanClassMk_of_mem_stratum` 📖	mathematical	`Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `stratum`	`ArchimedeanClass` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `ArchimedeanClass.instOrderTop`	—	`le_antisymm` `Mathlib.Tactic.Contrapose.contrapose₂` `IsOrderedModule.toPosSMulMono` `FiniteArchimedeanClass.mem_ball_iff` `Submodule.disjoint_def` `disjoint_ball_stratum` `FiniteArchimedeanClass.mem_closedBall_iff` `ball_sup_stratum_eq` `Submodule.mem_sup_right`
`archimedean_stratum` 📖	mathematical	—	`Archimedean` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `stratum` `Submodule.addCommMonoid` `Subtype.partialOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Submodule.toIsOrderedAddMonoid` `archimedeanClassMk_of_mem_stratum` `Subtype.prop` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass`
`ball_sup_stratum_eq` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `FiniteArchimedeanClass.ball` `IsOrderedModule.toPosSMulMono` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `stratum` `FiniteArchimedeanClass.closedBall`	—	—
`disjoint_ball_stratum` 📖	mathematical	—	`Disjoint` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `Submodule.instOrderBot` `FiniteArchimedeanClass.ball` `IsOrderedModule.toPosSMulMono` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `stratum`	—	—
`iSupIndep_stratum` 📖	mathematical	—	`iSupIndep` `FiniteArchimedeanClass` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.completeLattice` `stratum`	—	`Submodule.disjoint_def'` `Submodule.mem_iSup_iff_exists_dfinsupp'` `Mathlib.Tactic.Contrapose.contrapose₁` `DFinsupp.sum.eq_1` `Set.mem_of_mem_of_subset` `Subtype.prop` `instIsConcreteLE` `archimedeanClassMk_of_mem_stratum` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `ArchimedeanClass.mk_sum` `Finset.min'_mem` `Subtype.coe_ne_coe` `iSup_congr_Prop` `iSup_neg` `Finset.sum_congr`
`iSupIndep_stratum'` 📖	mathematical	—	`iSupIndep` `FiniteArchimedeanClass` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `baseDomain` `Submodule.addCommMonoid` `Submodule.module` `Submodule.completeLattice` `stratum'`	—	`iSupIndep_map_orderIso_iff` `iSupIndep.of_coe_Iic_comp` `Submodule.map_comap_subtype` `le_iSup` `iSupIndep_stratum`
`instNonempty` 📖	mathematical	—	`HahnEmbedding.ArchimedeanStrata`	—	`IsOrderedModule.toPosSMulMono` `IsModularLattice.exists_disjoint_and_sup_eq` `Submodule.instIsModularLattice` `Submodule.complementedLattice` `LT.lt.le` `FiniteArchimedeanClass.ball_lt_closedBall`
`isInternal_stratum'` 📖	mathematical	—	`DirectSum.IsInternal` `FiniteArchimedeanClass` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `baseDomain` `Submodule.addCommMonoid` `Submodule.module` `ArchimedeanClass` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `ArchimedeanClass.instOrderTop` `LinearOrder.toDecidableEq` `Submodule.addSubmonoidClass` `stratum'`	—	`DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top` `iSupIndep_stratum'` `Submodule.map_injective_of_injective` `RingHomSurjective.ids` `Submodule.subtype_injective` `iSup_congr` `le_iSup` `Submodule.map_iSup` `Submodule.map_comap_subtype` `Submodule.map_top` `Submodule.range_subtype`
`nontrivial_stratum` 📖	mathematical	—	`Nontrivial` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `stratum`	—	`Submodule.nontrivial_iff_ne_bot` `stratum_ne_bot`
`stratum_ne_bot` 📖	—	—	—	—	`Eq.not_lt` `IsOrderedModule.toPosSMulMono` `ball_sup_stratum_eq` `sup_of_le_left` `FiniteArchimedeanClass.ball_lt_closedBall`

HahnEmbedding.IsPartial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`baseEmbedding_le` 📖	mathematical	`HahnEmbedding.IsPartial`	`LinearPMap` `DivisionRing.toRing` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `Ring.toSemiring` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGroup.add_comm` `HahnSeries.instModule` `AddCommGroup.toAddCommMonoid` `LinearPMap.le` `HahnEmbedding.Seed.baseEmbedding`	—	`AddCommGroup.add_comm`
`strictMono` 📖	mathematical	`HahnEmbedding.IsPartial`	`StrictMono` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGroup.add_comm` `HahnSeries.instModule` `Subtype.preorder` `HahnSeries.instPartialOrderLex` `Subtype.instLinearOrder` `LinearPMap.toFun'`	—	`AddCommGroup.add_comm`
`truncLT_mem_range` 📖	mathematical	`HahnEmbedding.IsPartial`	`Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommGroup.toAddCommMonoid` `Submodule` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toSemiring` `DivisionRing.toRing` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGroup.add_comm` `HahnSeries.instModule` `SetLike.instMembership` `Submodule.setLike` `LinearMap.range` `LinearPMap.domain` `Submodule.addCommMonoid` `Submodule.module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearPMap.toFun` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `LinearMap` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `HahnSeries.instAddCommMonoid` `LinearMap.instFunLike` `HahnSeries.truncLTLinearMap` `Subtype.decidableLT` `LinearOrder.toDecidableLT` `ofLex` `LinearPMap.toFun'`	—	`AddCommGroup.add_comm`

HahnEmbedding.Partial

Definitions

Name	Category	Theorems
`eval` 📖	CompOp	5 math math: `eval_smul`, `eval_lt`, `eval_zero`, `eval_eq_truncLT`, `truncLT_eval_mem_range_extendFun`
`evalCoeff` 📖	CompOp	3 math math: `isWF_support_evalCoeff`, `evalCoeff_eq_zero`, `evalCoeff_eq`
`extend` 📖	CompOp	1 math math: `lt_extend`
`extendFun` 📖	CompOp	5 math math: `truncLT_mem_range_extendFun`, `extendFun_strictMono`, `isPartial_extendFun`, `baseEmbedding_le_extendFun`, `truncLT_eval_mem_range_extendFun`
`instInhabitedOfIsOrderedAddMonoid` 📖	CompOp	—
`sSup` 📖	CompOp	—
`sSupFun` 📖	CompOp	5 math math: `baseEmbedding_le_sSupFun`, `isPartial_sSupFun`, `truncLT_mem_range_sSupFun`, `le_sSupFun`, `sSupFun_strictMono`
`toOrderAddMonoidHom` 📖	CompOp	2 math math: `toOrderAddMonoidHom_apply`, `toOrderAddMonoidHom_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_of_mem_stratum` 📖	mathematical	`Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `HahnEmbedding.ArchimedeanStrata.stratum` `HahnEmbedding.Seed.toArchimedeanStrata` `Ring.toSemiring` `DivisionRing.toRing` `LinearPMap.domain` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `HahnSeries.instModule` `LinearPMap` `HahnEmbedding.IsPartial`	`LinearPMap.toFun'` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `ZeroHom` `HahnSeries.instZero` `ZeroHom.funLike` `HahnSeries.single` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.instFunLike` `HahnEmbedding.Seed.coeff`	—	`AddCommGroup.add_comm` `HahnEmbedding.Seed.mem_domain_baseEmbedding` `HahnEmbedding.IsPartial.baseEmbedding_le` `Subtype.prop` `DFinsupp.sum_single_index` `Equiv.injective` `ofLex_toLex` `HahnSeries.ext` `HahnEmbedding.Seed.coeff_baseEmbedding` `eq_or_ne` `DFinsupp.single_apply` `HahnSeries.coeff_single_same` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `HahnSeries.coeff_single_of_ne`
`archimedeanClassMk_eq_iff` 📖	mathematical	—	`Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `HahnSeries.instLinearOrderLex` `Subtype.instLinearOrder` `HahnSeries.instIsOrderedAddMonoidLex` `AddCommGroup.toAddCommMonoid` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `AddLeftCancelMonoid.toAddLeftCancelSemigroup` `AddCancelCommMonoid.toAddLeftCancelMonoid` `AddCommGroup.toAddCancelCommMonoid` `IsOrderedAddMonoid.toAddLeftMono` `LinearPMap.toFun'` `DivisionRing.toRing` `Lex.instModule'` `Ring.toSemiring` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `HahnSeries.instModule` `LinearPMap` `HahnEmbedding.IsPartial` `Submodule` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain`	—	`HahnSeries.instIsOrderedAddMonoidLex` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Submodule.toIsOrderedAddMonoid` `ArchimedeanClass.orderHom_injective` `toOrderAddMonoidHom_injective`
`archimedeanClassMk_le_of_eval_eq` 📖	mathematical	`eval` `LinearPMap.toFun'` `DivisionRing.toRing` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `Ring.toSemiring` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `HahnSeries.instModule` `AddCommGroup.toAddCommMonoid` `LinearPMap` `HahnEmbedding.IsPartial`	`SubNegMonoid.toSub` `Submodule` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain`	—	`Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.const_add_termg` `add_zero` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Abel.zero_termg` `ArchimedeanClass.mk_left_le_mk_add` `evalCoeff_eq` `IsOrderedModule.toPosSMulMono` `ArchimedeanClass.mk_sub_comm` `Submodule.addSubgroupClass` `LinearPMap.map_sub` `ofLex_sub` `HahnSeries.coeff_sub` `sub_eq_zero` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `coeff_ne_zero`
`baseEmbedding_le_extendFun` 📖	mathematical	`Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `HahnSeries.instModule` `LinearPMap` `HahnEmbedding.IsPartial`	`AddCommGroup.add_comm` `LinearPMap.le` `HahnEmbedding.Seed.baseEmbedding` `extendFun`	—	`AddCommGroup.add_comm` `extendFun.eq_1` `le_trans` `HahnEmbedding.IsPartial.baseEmbedding_le` `Subtype.prop` `LinearPMap.left_le_sup`
`baseEmbedding_le_sSupFun` 📖	mathematical	`Set.Nonempty` `HahnEmbedding.Partial` `DirectedOn` `LinearPMap` `DivisionRing.toRing` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `Ring.toSemiring` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `HahnSeries.instModule` `AddCommGroup.toAddCommMonoid` `LinearPMap.le` `HahnEmbedding.IsPartial`	`AddCommGroup.add_comm` `HahnEmbedding.Seed.baseEmbedding` `sSupFun`	—	`AddCommGroup.add_comm` `le_trans` `HahnEmbedding.IsPartial.baseEmbedding_le` `Subtype.prop` `le_sSupFun`
`coeff_eq_of_mem` 📖	mathematical	`Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `FiniteArchimedeanClass.ball` `IsOrderedModule.toPosSMulMono` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SubNegMonoid.toSub` `LinearPMap.domain` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `ArchimedeanClass.instOrderTop` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `HahnSeries.instModule` `LinearPMap` `HahnEmbedding.IsPartial`	`HahnSeries.coeff` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex` `LinearPMap.toFun'`	—	`IsOrderedModule.toPosSMulMono` `eq_of_sub_eq_zero` `HahnSeries.coeff_sub` `ofLex_sub` `Submodule.addSubgroupClass` `LinearPMap.map_sub` `coeff_eq_zero_of_mem` `sub_sub_sub_cancel_right` `Submodule.sub_mem`
`coeff_eq_zero_of_mem` 📖	mathematical	`Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `FiniteArchimedeanClass.ball` `IsOrderedModule.toPosSMulMono` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LinearPMap.domain` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `ArchimedeanClass.instOrderTop` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `HahnSeries.instModule` `LinearPMap` `HahnEmbedding.IsPartial`	`HahnSeries.coeff` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex` `LinearPMap.toFun'`	—	`IsOrderedModule.toPosSMulMono` `eq_or_ne` `LinearPMap.map_zero` `HahnSeries.coeff_eq_zero_of_lt_orderTop` `Mathlib.Tactic.ApplyFun.lt_of_lt` `orderTop_eq_archimedeanClassMk` `FiniteArchimedeanClass.withTopOrderIso_apply_coe` `lt_of_le_of_lt` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass`
`coeff_ne_zero` 📖	—	—	—	—	`HahnSeries.coeff_orderTop_ne` `orderTop_eq_finiteArchimedeanClassMk`
`evalCoeff_eq` 📖	mathematical	`Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `FiniteArchimedeanClass.ball` `IsOrderedModule.toPosSMulMono` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SubNegMonoid.toSub` `LinearPMap.domain` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `ArchimedeanClass.instOrderTop` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `HahnSeries.instModule` `LinearPMap` `HahnEmbedding.IsPartial`	`evalCoeff` `HahnSeries.coeff` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex` `LinearPMap.toFun'`	—	`IsOrderedModule.toPosSMulMono` `coeff_eq_of_mem` `le_rfl`
`evalCoeff_eq_zero` 📖	mathematical	`Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `FiniteArchimedeanClass.ball` `IsOrderedModule.toPosSMulMono` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SubNegMonoid.toSub` `LinearPMap.domain` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `ArchimedeanClass.instOrderTop` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `HahnSeries.instModule` `LinearPMap` `HahnEmbedding.IsPartial`	`evalCoeff`	—	`IsOrderedModule.toPosSMulMono` `evalCoeff.eq_1`
`eval_eq_truncLT` 📖	mathematical	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `SubNegMonoid.toAddMonoid` `HahnSeries.instModule` `LinearPMap` `HahnEmbedding.IsPartial` `FiniteArchimedeanClass.ball` `IsOrderedModule.toPosSMulMono` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`eval` `DFunLike.coe` `Equiv` `AddCommMonoid.toAddMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `LinearMap` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `HahnSeries.instAddCommMonoid` `LinearMap.instFunLike` `HahnSeries.truncLTLinearMap` `Subtype.decidableLT` `LinearOrder.toDecidableLT` `ofLex` `LinearPMap.toFun'`	—	`IsOrderedModule.toPosSMulMono` `Equiv.injective` `HahnSeries.ext` `lt_or_ge` `HahnSeries.coe_truncLTLinearMap` `HahnSeries.coeff_truncLT_of_lt` `evalCoeff_eq` `Subtype.coe_eta` `HahnSeries.coeff_truncLT_of_le` `evalCoeff_eq_zero` `Mathlib.Tactic.Contrapose.contrapose₃` `Mathlib.Tactic.Push.not_forall_eq` `StrictAnti.antitone` `FiniteArchimedeanClass.ball_strictAnti`
`eval_lt` 📖	mathematical	`Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `HahnSeries.instModule` `LinearPMap` `HahnEmbedding.IsPartial` `Preorder.toLT`	`HahnSeries.instPartialOrderLex` `Subtype.instLinearOrder` `eval` `LinearPMap.toFun'`	—	`HahnSeries.lt_iff` `sub_ne_zero_of_ne` `LT.lt.ne` `evalCoeff_eq` `IsOrderedModule.toPosSMulMono` `val_sub_ne_zero` `exists_sub_mem_ball` `sub_lt_sub_iff_right` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `ArchimedeanClass.lt_of_mk_lt_mk_of_nonneg` `sub_nonneg_of_le` `LT.lt.le` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.const_add_termg` `add_zero` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Abel.zero_termg` `ArchimedeanClass.mk_sub_comm` `ArchimedeanClass.mk_add_eq_mk_left` `AddCommGroup.add_comm` `StrictMono.lt_iff_lt` `HahnEmbedding.IsPartial.strictMono` `Subtype.prop` `le_antisymm` `Mathlib.Tactic.Contrapose.contrapose₁` `HahnSeries.coeff_sub` `ofLex_sub` `Submodule.addSubgroupClass` `LinearPMap.map_sub` `coeff_ne_zero` `sub_eq_zero_of_eq` `Eq.le` `coeff_eq_of_mem` `sub_self` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass`
`eval_ne` 📖	—	`Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `HahnSeries.instModule` `LinearPMap` `HahnEmbedding.IsPartial`	—	—	`val_sub_ne_zero` `sub_ne_zero` `IsOrderedModule.toPosSMulMono` `le_refl` `Submodule.mem_sup` `HahnEmbedding.ArchimedeanStrata.ball_sup_stratum_eq` `add_sub_cancel_right` `Submodule.add_mem` `mem_domain` `Mathlib.Tactic.Contrapose.contrapose₁` `eq_or_ne` `Ne.lt_top` `FiniteArchimedeanClass.mem_ball_iff` `archimedeanClassMk_le_of_eval_eq`
`eval_smul` 📖	mathematical	—	`eval` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Lex.instSMul` `HahnSeries.instSMul`	—	`eval.congr_simp` `zero_smul` `eval_zero` `toLex_smul` `Equiv.injective` `HahnSeries.ext` `IsOrderedModule.toPosSMulMono` `IsScalarTower.left` `smul_sub` `Submodule.smul_mem` `evalCoeff_eq` `LinearPMap.map_smul` `Mathlib.Tactic.Contrapose.contrapose₄` `smul_smul` `inv_mul_cancel₀` `one_smul` `evalCoeff_eq_zero` `smul_zero`
`eval_zero` 📖	mathematical	—	`eval` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `instZeroLex` `HahnSeries.instZero`	—	`evalCoeff_eq` `IsOrderedModule.toPosSMulMono` `sub_self` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `LinearPMap.map_zero` `HahnSeries.isPWO_support'` `toLex_zero`
`exists_domain_eq_top` 📖	mathematical	—	`LinearPMap.domain` `DivisionRing.toRing` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `Ring.toSemiring` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `HahnSeries.instModule` `AddCommGroup.toAddCommMonoid` `LinearPMap` `HahnEmbedding.IsPartial` `Submodule` `Submodule.instTop`	—	`exists_isMax` `Submodule.eq_top_iff'` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `lt_extend` `isMax_iff_forall_not_lt`
`exists_isMax` 📖	mathematical	—	`IsMax` `HahnEmbedding.Partial` `LinearPMap` `DivisionRing.toRing` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `Ring.toSemiring` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `HahnSeries.instModule` `AddCommGroup.toAddCommMonoid` `LinearPMap.le` `HahnEmbedding.IsPartial`	—	`zorn_le_nonempty` `IsChain.directedOn` `instReflLe` `mem_upperBounds` `le_sSupFun`
`exists_sub_mem_ball` 📖	mathematical	`Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `HahnSeries.instModule` `LinearPMap` `HahnEmbedding.IsPartial`	`FiniteArchimedeanClass.ball` `IsOrderedModule.toPosSMulMono` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SubNegMonoid.toSub` `val_sub_ne_zero`	—	`val_sub_ne_zero` `IsOrderedModule.toPosSMulMono` `eval_eq_truncLT` `AddCommGroup.add_comm` `RingHomSurjective.ids` `LinearMap.mem_range` `HahnEmbedding.IsPartial.truncLT_mem_range` `Subtype.prop` `Mathlib.Tactic.Contrapose.contrapose₁` `eval_ne`
`extendFun_strictMono` 📖	mathematical	`Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `HahnSeries.instModule` `LinearPMap` `HahnEmbedding.IsPartial`	`StrictMono` `AddCommGroup.add_comm` `extendFun` `Subtype.preorder` `HahnSeries.instPartialOrderLex` `Subtype.instLinearOrder` `LinearPMap.toFun'`	—	`Mathlib.Tactic.Contrapose.contrapose₄` `Submodule.smul_mem_iff` `IsScalarTower.left` `neg_mem_iff` `AddSubgroupClass.toNegMemClass` `Submodule.addSubgroupClass` `neg_smul` `AddCommGroup.add_comm` `lt_of_sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddLex` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `HahnSeries.instIsOrderedAddMonoidLex` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `LinearPMap.map_sub` `Submodule.mem_sup` `LinearPMap.domain_supSpanSingleton` `extendFun.eq_1` `Subtype.prop` `sub_pos` `AddMemClass.isRightCancelAdd` `AddSubmonoidClass.toAddMemClass` `Submodule.addSubmonoidClass` `Submodule.toIsOrderedAddMonoid` `Submodule.mem_span_singleton` `neg_lt_iff_pos_add` `HahnEmbedding.IsPartial.strictMono` `neg_zero` `zero_smul` `eval.congr_simp` `eval_zero` `LinearPMap.map_zero` `eval_lt` `eval_smul`
`isPartial_extendFun` 📖	mathematical	`Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `HahnSeries.instModule` `LinearPMap` `HahnEmbedding.IsPartial`	`extendFun`	—	`extendFun_strictMono` `baseEmbedding_le_extendFun` `truncLT_mem_range_extendFun`
`isPartial_sSupFun` 📖	mathematical	`Set.Nonempty` `HahnEmbedding.Partial` `DirectedOn` `LinearPMap` `DivisionRing.toRing` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `Ring.toSemiring` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `HahnSeries.instModule` `AddCommGroup.toAddCommMonoid` `LinearPMap.le` `HahnEmbedding.IsPartial`	`sSupFun`	—	`sSupFun_strictMono` `baseEmbedding_le_sSupFun` `truncLT_mem_range_sSupFun`
`isWF_support_evalCoeff` 📖	mathematical	—	`Set.IsWF` `FiniteArchimedeanClass` `ArchimedeanClass` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `ArchimedeanClass.instOrderTop` `Function.support` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `evalCoeff`	—	`Set.isWF_iff_no_descending_seq` `Mathlib.Tactic.Push.not_forall_eq` `IsOrderedModule.toPosSMulMono` `Mathlib.Tactic.Contrapose.contrapose₁` `Function.mem_support` `evalCoeff_eq` `StrictAnti.antitone` `FiniteArchimedeanClass.ball_strictAnti` `Nat.instCanonicallyOrderedAdd` `HahnSeries.isWF_support`
`le_sSupFun` 📖	mathematical	`DirectedOn` `HahnEmbedding.Partial` `LinearPMap` `DivisionRing.toRing` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `Ring.toSemiring` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `HahnSeries.instModule` `AddCommGroup.toAddCommMonoid` `LinearPMap.le` `HahnEmbedding.IsPartial` `Set` `Set.instMembership`	`sSupFun`	—	`LinearPMap.le_sSup` `Set.mem_image`
`lt_extend` 📖	mathematical	`Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `HahnSeries.instModule` `LinearPMap` `HahnEmbedding.IsPartial`	`HahnEmbedding.Partial` `Preorder.toLT` `LinearPMap.semilatticeInf` `extend`	—	`lt_of_le_of_ne` `LinearPMap.left_le_sup` `Mathlib.Tactic.Contrapose.contrapose₂` `Submodule.mem_sup_right`
`mem_domain` 📖	mathematical	`Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `HahnEmbedding.ArchimedeanStrata.stratum` `HahnEmbedding.Seed.toArchimedeanStrata`	`Ring.toSemiring` `DivisionRing.toRing` `LinearPMap.domain` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `HahnSeries.instModule` `LinearPMap` `HahnEmbedding.IsPartial`	—	`Set.mem_of_subset_of_mem` `AddCommGroup.add_comm` `HahnEmbedding.IsPartial.baseEmbedding_le` `Subtype.prop` `HahnEmbedding.Seed.mem_domain_baseEmbedding`
`orderTop_eq_archimedeanClassMk` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `WithTop` `FiniteArchimedeanClass` `ArchimedeanClass` `Preorder.toLE` `WithTop.instPreorder` `Subtype.preorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `ArchimedeanClass.instOrderTop` `instFunLikeOrderIso` `FiniteArchimedeanClass.withTopOrderIso` `HahnSeries.orderTop` `Subtype.partialOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Equiv` `Lex` `HahnSeries` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex` `LinearPMap.toFun'` `DivisionRing.toRing` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `Ring.toSemiring` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `HahnSeries.instModule` `AddCommGroup.toAddCommMonoid` `LinearPMap` `HahnEmbedding.IsPartial` `Submodule` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain`	—	`LinearPMap.map_zero` `HahnSeries.orderTop_zero` `TopHomClass.map_top` `InfTopHomClass.toTopHomClass` `OrderIsoClass.toInfTopHomClass` `OrderIso.instOrderIsoClass` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `exists_ne` `HahnEmbedding.ArchimedeanStrata.nontrivial_stratum` `HahnEmbedding.ArchimedeanStrata.archimedeanClassMk_of_mem_stratum` `mem_domain` `Iff.ne` `LinearMap.map_eq_zero_iff` `StrictMono.injective` `HahnEmbedding.Seed.strictMono_coeff` `HahnSeries.orderTop_single` `ofLex_toLex` `apply_of_mem_stratum` `orderTop_eq_iff` `FiniteArchimedeanClass.withTopOrderIso_apply_coe`
`orderTop_eq_finiteArchimedeanClassMk` 📖	mathematical	—	`HahnSeries.orderTop` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `DFunLike.coe` `Equiv` `Lex` `HahnSeries` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex` `LinearPMap.toFun'` `DivisionRing.toRing` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `Ring.toSemiring` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `HahnSeries.instModule` `AddCommGroup.toAddCommMonoid` `LinearPMap` `HahnEmbedding.IsPartial` `WithTop.some` `Submodule` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain`	—	`Equiv.injective` `orderTop_eq_archimedeanClassMk` `FiniteArchimedeanClass.withTopOrderIso_apply_coe`
`orderTop_eq_iff` 📖	mathematical	—	`HahnSeries.orderTop` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `DFunLike.coe` `Equiv` `Lex` `HahnSeries` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex` `LinearPMap.toFun'` `DivisionRing.toRing` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `Ring.toSemiring` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `HahnSeries.instModule` `AddCommGroup.toAddCommMonoid` `LinearPMap` `HahnEmbedding.IsPartial` `Submodule` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain`	—	`subsingleton_or_nontrivial` `FiniteArchimedeanClass.instNonemptyOfNontrivial` `Function.Injective.nontrivial` `HahnEmbedding.ArchimedeanStrata.nontrivial_stratum` `StrictMono.injective` `HahnEmbedding.Seed.strictMono_coeff` `HahnSeries.instIsOrderedAddMonoidLex` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `archimedeanClassMk_eq_iff` `OrderIso.injective`
`sSupFun_strictMono` 📖	mathematical	`Set.Nonempty` `HahnEmbedding.Partial` `DirectedOn` `LinearPMap` `DivisionRing.toRing` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `Ring.toSemiring` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `HahnSeries.instModule` `AddCommGroup.toAddCommMonoid` `LinearPMap.le` `HahnEmbedding.IsPartial`	`StrictMono` `Submodule` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain` `AddCommGroup.add_comm` `sSupFun` `Subtype.preorder` `HahnSeries.instPartialOrderLex` `Subtype.instLinearOrder` `LinearPMap.toFun'`	—	`AddCommGroup.add_comm` `lt_of_sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddLex` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `HahnSeries.instIsOrderedAddMonoidLex` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Submodule.addSubgroupClass` `LinearPMap.map_sub` `DirectedOn.mono_comp` `LinearPMap.mem_domain_sSup_iff` `Set.Nonempty.image` `Subtype.prop` `LinearPMap.sSup_apply` `Set.mem_image` `HahnEmbedding.IsPartial.strictMono` `LinearPMap.map_zero` `Subtype.coe_lt_coe`
`toOrderAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidHom` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `HahnSeries.instModule` `LinearPMap` `HahnEmbedding.IsPartial` `Subtype.preorder` `HahnSeries.instPartialOrderLex` `Subtype.instLinearOrder` `AddMonoid.toAddZeroClass` `Submodule.addCommGroup` `instAddZeroClassLex` `HahnSeries.instAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `OrderAddMonoidHom.instFunLike` `toOrderAddMonoidHom` `LinearPMap.toFun'`	—	—
`toOrderAddMonoidHom_injective` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `HahnSeries.instModule` `LinearPMap` `HahnEmbedding.IsPartial` `DFunLike.coe` `OrderAddMonoidHom` `Subtype.preorder` `HahnSeries.instPartialOrderLex` `Subtype.instLinearOrder` `AddMonoid.toAddZeroClass` `Submodule.addCommGroup` `instAddZeroClassLex` `HahnSeries.instAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `OrderAddMonoidHom.instFunLike` `toOrderAddMonoidHom`	—	`StrictMono.injective` `AddCommGroup.add_comm` `HahnEmbedding.IsPartial.strictMono` `Subtype.prop`
`truncLT_eval_mem_range_extendFun` 📖	mathematical	`Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `HahnSeries.instModule` `LinearPMap` `HahnEmbedding.IsPartial`	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommGroup.add_comm` `LinearMap.range` `extendFun` `Submodule.addCommMonoid` `Submodule.module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearPMap.toFun` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `LinearMap` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `HahnSeries.instAddCommMonoid` `LinearMap.instFunLike` `HahnSeries.truncLTLinearMap` `Subtype.decidableLT` `LinearOrder.toDecidableLT` `ofLex` `eval`	—	`AddCommGroup.add_comm` `RingHomSurjective.ids` `extendFun.eq_1` `LinearMap.mem_range` `IsOrderedModule.toPosSMulMono` `HahnEmbedding.IsPartial.truncLT_mem_range` `Subtype.prop` `Submodule.mem_sup_left` `LinearPMap.toFun_eq_coe` `LinearPMap.supSpanSingleton_apply_mk_of_mem` `HahnSeries.ext` `lt_or_ge` `HahnSeries.coe_truncLTLinearMap` `HahnSeries.coeff_truncLT_of_lt` `evalCoeff_eq` `Set.mem_of_mem_of_subset` `instIsConcreteLE` `LT.lt.le` `FiniteArchimedeanClass.ball_strictAnti` `HahnSeries.coeff_truncLT_of_le` `Submodule.mem_sup_right` `Submodule.mem_span_singleton_self` `Equiv.injective` `ofLex_toLex` `LinearPMap.supSpanSingleton_apply_self` `eval.eq_1` `evalCoeff_eq_zero` `Mathlib.Tactic.Contrapose.contrapose₄` `StrictAnti.antitone`
`truncLT_mem_range_extendFun` 📖	mathematical	`Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `HahnSeries.instModule` `LinearPMap` `HahnEmbedding.IsPartial`	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommGroup.add_comm` `LinearMap.range` `extendFun` `Submodule.addCommMonoid` `Submodule.module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearPMap.toFun` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `LinearMap` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `HahnSeries.instAddCommMonoid` `LinearMap.instFunLike` `HahnSeries.truncLTLinearMap` `Subtype.decidableLT` `LinearOrder.toDecidableLT` `ofLex` `LinearPMap.toFun'`	—	`AddCommGroup.add_comm` `RingHomSurjective.ids` `Submodule.mem_sup` `LinearPMap.domain_supSpanSingleton` `extendFun.eq_1` `Submodule.mem_span_singleton` `ofLex_add` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `toLex_add` `ofLex_smul` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `toLex_smul` `Submodule.add_mem` `LinearMap.mem_range` `HahnEmbedding.IsPartial.truncLT_mem_range` `Subtype.prop` `Submodule.mem_sup_left` `LinearPMap.supSpanSingleton_apply_mk_of_mem` `Submodule.smul_mem` `truncLT_eval_mem_range_extendFun`
`truncLT_mem_range_sSupFun` 📖	mathematical	`Set.Nonempty` `HahnEmbedding.Partial` `DirectedOn` `LinearPMap` `DivisionRing.toRing` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `Ring.toSemiring` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `HahnSeries.instModule` `AddCommGroup.toAddCommMonoid` `LinearPMap.le` `HahnEmbedding.IsPartial`	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Submodule` `AddCommGroup.add_comm` `SetLike.instMembership` `Submodule.setLike` `LinearMap.range` `LinearPMap.domain` `sSupFun` `Submodule.addCommMonoid` `Submodule.module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearPMap.toFun` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `LinearMap` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `HahnSeries.instAddCommMonoid` `LinearMap.instFunLike` `HahnSeries.truncLTLinearMap` `Subtype.decidableLT` `LinearOrder.toDecidableLT` `ofLex` `LinearPMap.toFun'`	—	`AddCommGroup.add_comm` `RingHomSurjective.ids` `DirectedOn.mono_comp` `LinearPMap.mem_domain_sSup_iff` `Set.Nonempty.image` `Subtype.prop` `Set.mem_image` `HahnEmbedding.IsPartial.truncLT_mem_range` `Set.mem_of_mem_of_subset` `le_sSupFun` `LinearPMap.sSup_apply` `HahnSeries.coe_truncLTLinearMap`
`val_sub_ne_zero` 📖	—	`Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `HahnSeries.instModule` `LinearPMap` `HahnEmbedding.IsPartial`	—	—	`Mathlib.Tactic.Contrapose.contrapose₄` `sub_eq_zero`

HahnEmbedding.Seed

Definitions

Name	Category	Theorems
`baseEmbedding` 📖	CompOp	8 math math: `HahnEmbedding.IsPartial.baseEmbedding_le`, `HahnEmbedding.Partial.baseEmbedding_le_sSupFun`, `baseEmbedding_strictMono`, `isPartial_baseEmbedding`, `truncLT_mem_range_baseEmbedding`, `mem_domain_baseEmbedding`, `HahnEmbedding.Partial.baseEmbedding_le_extendFun`, `domain_baseEmbedding`
`coeff` 📖	CompOp	4 math math: `strictMono_coeff`, `coeff_baseEmbedding`, `hahnCoeff_apply`, `HahnEmbedding.Partial.apply_of_mem_stratum`
`coeff'` 📖	CompOp	—
`hahnCoeff` 📖	CompOp	1 math math: `hahnCoeff_apply`
`toArchimedeanStrata` 📖	CompOp	2 math math: `strictMono_coeff`, `domain_baseEmbedding`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`baseEmbedding_pos` 📖	mathematical	`Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGroup.add_comm` `HahnSeries.instModule` `baseEmbedding` `Preorder.toLT` `Submodule.zero`	`HahnSeries.instPartialOrderLex` `Subtype.instLinearOrder` `instZeroLex` `HahnSeries.instZero` `LinearPMap.toFun'`	—	`AddCommGroup.add_comm` `Subtype.prop` `Submodule.mem_iSup_iff_exists_dfinsupp'` `Mathlib.Tactic.Contrapose.contrapose₂` `DFinsupp.sum_eq_zero` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `DFinsupp.notMem_support_iff` `Finset.eq_empty_iff_forall_notMem` `LT.lt.ne` `HahnSeries.lt_iff` `coeff_baseEmbedding` `Mathlib.Tactic.Contrapose.contrapose₃` `Subtype.coe_le_coe` `Finset.min'_le` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `ArchimedeanClass.pos_of_pos_of_mk_lt` `ArchimedeanClass.mk_sub_comm` `sub_eq_of_eq_add` `Finset.sum_erase_add` `Finset.min'_mem` `HahnEmbedding.ArchimedeanStrata.archimedeanClassMk_of_mem_stratum` `DFinsupp.sum.eq_1` `ArchimedeanClass.mk_sum` `StrictMonoOn.mono` `Finset.coe_erase` `Finset.mem_erase` `Finset.min'_lt_of_mem_erase_min'` `Finset.sum_congr` `Ne.lt_top` `strictMono_coeff`
`baseEmbedding_strictMono` 📖	mathematical	—	`StrictMono` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGroup.add_comm` `HahnSeries.instModule` `baseEmbedding` `Subtype.preorder` `HahnSeries.instPartialOrderLex` `Subtype.instLinearOrder` `LinearPMap.toFun'`	—	`AddCommGroup.add_comm` `lt_of_sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddLex` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `HahnSeries.instIsOrderedAddMonoidLex` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Submodule.addSubgroupClass` `LinearPMap.map_sub` `baseEmbedding_pos` `AddMemClass.isRightCancelAdd` `AddSubmonoidClass.toAddMemClass` `Submodule.addSubmonoidClass` `Submodule.toIsOrderedAddMonoid`
`coeff_baseEmbedding` 📖	mathematical	`Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `LinearPMap.domain` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGroup.add_comm` `HahnSeries.instModule` `baseEmbedding` `DFinsupp.sum` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `HahnEmbedding.ArchimedeanStrata.stratum` `toArchimedeanStrata` `LinearOrder.toDecidableEq` `Submodule.zero` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.instFunLike` `Submodule.subtype`	`HahnSeries.coeff` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex` `LinearPMap.toFun'` `coeff` `DFinsupp` `DFinsupp.instDFunLike`	—	`AddCommGroup.add_comm` `hahnCoeff_apply`
`domain_baseEmbedding` 📖	mathematical	—	`LinearPMap.domain` `DivisionRing.toRing` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `Ring.toSemiring` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGroup.add_comm` `HahnSeries.instModule` `AddCommGroup.toAddCommMonoid` `baseEmbedding` `HahnEmbedding.ArchimedeanStrata.baseDomain` `toArchimedeanStrata`	—	`AddCommGroup.add_comm`
`hahnCoeff_apply` 📖	mathematical	`Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `HahnEmbedding.ArchimedeanStrata.baseDomain` `toArchimedeanStrata` `DFinsupp.sum` `FiniteArchimedeanClass` `HahnEmbedding.ArchimedeanStrata.stratum` `ArchimedeanClass` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `ArchimedeanClass.instOrderTop` `LinearOrder.toDecidableEq` `Submodule.zero` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.instFunLike` `Submodule.subtype`	`DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `DirectSum` `instAddCommMonoidDirectSum` `DirectSum.instModule` `hahnCoeff` `coeff`	—	`Submodule.addSubmonoidClass` `Set.mem_of_mem_of_subset` `Subtype.prop` `instIsConcreteLE` `le_iSup` `Submodule.subtype_injective` `DirectSum.coeAddMonoidHom_eq_dfinsuppSum` `DFinsupp.sum_mapRange_index` `map_dfinsuppSum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Equiv.apply_symm_apply`
`isPartial_baseEmbedding` 📖	mathematical	—	`HahnEmbedding.IsPartial` `baseEmbedding`	—	`baseEmbedding_strictMono` `le_refl` `AddCommGroup.add_comm` `truncLT_mem_range_baseEmbedding`
`mem_domain_baseEmbedding` 📖	mathematical	`Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `HahnEmbedding.ArchimedeanStrata.stratum` `toArchimedeanStrata`	`Ring.toSemiring` `DivisionRing.toRing` `LinearPMap.domain` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGroup.add_comm` `HahnSeries.instModule` `baseEmbedding`	—	`Set.mem_of_mem_of_subset` `AddCommGroup.add_comm` `domain_baseEmbedding` `instIsConcreteLE` `le_iSup_iff`
`strictMono_coeff` 📖	mathematical	—	`StrictMono` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `HahnEmbedding.ArchimedeanStrata.stratum` `toArchimedeanStrata` `Subtype.preorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.instFunLike` `coeff`	—	—
`truncLT_mem_range_baseEmbedding` 📖	mathematical	—	`Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommGroup.toAddCommMonoid` `Submodule` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toSemiring` `DivisionRing.toRing` `instAddCommGroupLex` `HahnSeries.instAddCommGroup` `Lex.instModule'` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommGroup.add_comm` `HahnSeries.instModule` `SetLike.instMembership` `Submodule.setLike` `LinearMap.range` `LinearPMap.domain` `baseEmbedding` `Submodule.addCommMonoid` `Submodule.module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearPMap.toFun` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `LinearMap` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `HahnSeries.instAddCommMonoid` `LinearMap.instFunLike` `HahnSeries.truncLTLinearMap` `Subtype.decidableLT` `LinearOrder.toDecidableLT` `ofLex` `LinearPMap.toFun'`	—	`AddCommGroup.add_comm` `Subtype.prop` `RingHomSurjective.ids` `Submodule.mem_iSup_iff_exists_dfinsupp'` `domain_baseEmbedding` `HahnEmbedding.ArchimedeanStrata.baseDomain.eq_1` `Equiv.injective` `ofLex_toLex` `LinearPMap.toFun_eq_coe` `HahnSeries.ext` `coeff_baseEmbedding` `lt_or_ge` `HahnSeries.coe_truncLTLinearMap` `HahnSeries.coeff_truncLT_of_lt` `not_le_of_gt` `HahnSeries.coeff_truncLT_of_le` `LinearMap.map_zero`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hahnEmbedding_isOrderedModule` 📖	mathematical	—	`StrictMono` `Lex` `HahnSeries` `FiniteArchimedeanClass` `Subtype.partialOrder` `ArchimedeanClass` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.instLinearOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instOrderTop` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `HahnSeries.instPartialOrderLex` `Subtype.instLinearOrder` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instAddCommMonoidLex` `HahnSeries.instAddCommMonoid` `Lex.instModule'` `HahnSeries.instModule` `LinearMap.instFunLike` `OrderIso` `WithTop` `WithTop.instPreorder` `Subtype.preorder` `instFunLikeOrderIso` `FiniteArchimedeanClass.withTopOrderIso` `HahnSeries.orderTop` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	`HahnEmbedding.Partial.exists_domain_eq_top` `RingHomCompTriple.ids` `StrictMono.comp` `AddCommGroup.add_comm` `HahnEmbedding.IsPartial.strictMono` `HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk`

---

← Back to Index