Commit 2023-12-25 18:05 b1556bbb
View on Github →feat(Data/Polynomial/Expand): add leadingCoeff_expand and monic_expand_iff (#9261)
The first states that expand preserves leading coefficient; the second states that expand preserves monicity, hence gives a converse to Monic.expand.