Theorem HahnSeries.embDomainOrderAddMonoidHom_injective

Modification history

2025-09-09 20:10
Mathlib/RingTheory/HahnSeries/Lex.lean
feat(RingTheory/HahnSeries): embDomain as OrderAddMonoidHom; orderTop of embDomain (#29421) …
Added HahnSeries.embDomainOrderAddMonoidHom_injectiveView on Github →