instModule' 📖 | CompOp | 22 mathmath: HahnEmbedding.IsPartial.baseEmbedding_le, HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk, HahnEmbedding.Partial.archimedeanClassMk_eq_iff, HahnEmbedding.Seed.baseEmbedding_strictMono, HahnEmbedding.Partial.toOrderAddMonoidHom_apply, symm_toLexLinearEquiv, HahnEmbedding.Partial.orderTop_eq_iff, HahnEmbedding.IsPartial.strictMono, HahnEmbedding.IsPartial.truncLT_mem_range, coe_toLexLinearEquiv, HahnEmbedding.Partial.orderTop_eq_finiteArchimedeanClassMk, hahnEmbedding_isOrderedModule_rat, HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding, HahnEmbedding.Partial.mem_domain, HahnEmbedding.Seed.mem_domain_baseEmbedding, HahnEmbedding.Partial.exists_domain_eq_top, HahnEmbedding.Partial.exists_isMax, HahnEmbedding.Seed.domain_baseEmbedding, coe_ofLexLinearEquiv, hahnEmbedding_isOrderedModule, symm_ofLexLinearEquiv, HahnEmbedding.Partial.toOrderAddMonoidHom_injective
|