Theorem Multiplicative.toAdd_image_setMul

Modification history

2026-02-02 07:19
Mathlib/Algebra/Group/TypeTags/Pointwise.lean
feat(RingTheory/MvPolynomial): powers of ideal of variables (#33539) …
Added Multiplicative.toAdd_image_setMulView on Github →