Theorem Multiplicative.ofAdd_eq_top

Modification history

2025-11-18 16:33
Mathlib/Algebra/Order/Monoid/Unbundled/TypeTags.lean
feat: characterise regular elements of type synonyms (#31739)
Added Multiplicative.ofAdd_eq_topView on Github →