HahnEmbedding

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

Statistics

Metric	Count
Definitions	0
Theorems hahnEmbedding_isOrderedAddMonoid, hahnEmbedding_isOrderedModule_rat, instNonemptySeedRatReal	3
Total	3

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hahnEmbedding_isOrderedAddMonoid 📖	mathematical	—	Lex HahnSeries FiniteArchimedeanClass Real Subtype.partialOrder ArchimedeanClass SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ArchimedeanClass.instLinearOrder Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder ArchimedeanClass.instOrderTop Real.instZero DFunLike.coe OrderAddMonoidHom HahnSeries.instPartialOrderLex Subtype.instLinearOrder Real.partialOrder AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddZeroClassLex HahnSeries.instAddMonoid Real.instAddMonoid OrderAddMonoidHom.instFunLike OrderIso WithTop WithTop.instPreorder Subtype.preorder instFunLikeOrderIso FiniteArchimedeanClass.withTopOrderIso HahnSeries.orderTop Equiv EquivLike.toFunLike Equiv.instEquivLike ofLex	—	IsOrderedAddMonoid.toIsOrderedCancelAddMonoid DivisibleHull.coe_injective instIsAddTorsionFreeOfAddLeftStrictMonoOfAddRightStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedCancelAddMonoid.toIsOrderedAddMonoid DivisibleHull.instIsOrderedCancelAddMonoid RCLike.charZero_rclike hahnEmbedding_isOrderedModule_rat IsStrictOrderedModule.toIsOrderedModule DivisibleHull.instIsStrictOrderedModuleRat StrictMono.monotone StrictMono.injective HahnSeries.embDomainOrderAddMonoidHom_injective OrderIso.symm_apply_eq HahnSeries.orderTop_embDomain OrderAddMonoidHom.instAddMonoidHomClass TopHomClass.map_top InfTopHomClass.toTopHomClass OrderIsoClass.toInfTopHomClass OrderIso.instOrderIsoClass FiniteArchimedeanClass.withTopOrderIso_apply_coe OrderIso.symm_apply_apply
hahnEmbedding_isOrderedModule_rat 📖	mathematical	—	StrictMono Lex HahnSeries FiniteArchimedeanClass Real Subtype.partialOrder ArchimedeanClass SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ArchimedeanClass.instLinearOrder Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder ArchimedeanClass.instOrderTop Real.instZero HahnSeries.instPartialOrderLex Subtype.instLinearOrder Real.partialOrder DFunLike.coe LinearMap Rat.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommMonoidLex HahnSeries.instAddCommMonoid Real.instAddCommMonoid Lex.instModule' HahnSeries.instModule NormedSpace.toModule Rat.instNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedAlgebra.toNormedSpace SeminormedCommRing.toSeminormedRing normedAlgebraRat NormedField.toNormedDivisionRing Real.normedField RCLike.charZero_rclike Real.instRCLike RCLike.toNormedAlgebra LinearMap.instFunLike OrderIso WithTop WithTop.instPreorder Subtype.preorder instFunLikeOrderIso FiniteArchimedeanClass.withTopOrderIso HahnSeries.orderTop Equiv EquivLike.toFunLike Equiv.instEquivLike ofLex	—	hahnEmbedding_isOrderedModule IsStrictOrderedRing.toIsOrderedRing Rat.instIsStrictOrderedRing instArchimedeanRat RCLike.charZero_rclike Real.instIsOrderedAddMonoid Real.instArchimedean instNonemptySeedRatReal
instNonemptySeedRatReal 📖	mathematical	—	HahnEmbedding.Seed Rat.instDivisionRing Rat.linearOrder IsStrictOrderedRing.toIsOrderedRing DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Rat.instIsStrictOrderedRing instArchimedeanRat Real Real.instAddCommGroup Real.linearOrder NormedSpace.toModule Rat.instNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedAlgebra.toNormedSpace SeminormedCommRing.toSeminormedRing normedAlgebraRat NormedField.toNormedDivisionRing Real.normedField RCLike.charZero_rclike Real.instRCLike RCLike.toNormedAlgebra	—	IsStrictOrderedRing.toIsOrderedRing Rat.instIsStrictOrderedRing instArchimedeanRat RCLike.charZero_rclike HahnEmbedding.ArchimedeanStrata.instNonempty Monotone.strictMono_of_injective OrderHomClass.monotone OrderAddMonoidHom.instOrderHomClass Archimedean.exists_orderAddMonoidHom_real_injective Submodule.toIsOrderedAddMonoid HahnEmbedding.ArchimedeanStrata.archimedean_stratum

---

← Back to Index