mathlib
fc6f9673 - chore(ring_theory/hahn_series): emb_domain_add needs only add_monoid, not semiring (#7802)

Commit

4 years ago

chore(ring_theory/hahn_series): emb_domain_add needs only add_monoid, not semiring (#7802) This is my fault, the lemma ended up in the wrong place in #7737

Author

eric-wieser

Parents

54d8b94e

mathlib fc6f9673 - chore(ring_theory/hahn_series): emb_domain_add needs only add_monoid, not semiring (#7802)

mathlib
fc6f9673 - chore(ring_theory/hahn_series): emb_domain_add needs only add_monoid, not semiring (#7802)