Theorem UniqueFactorizationMonoid.finprod_pow_count_eq_of_subsingleton_units

Modification history

2026-03-11 20:11
Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean
feat(RingTheory/UniqueFactorizationDomain/Multiplicity): more API (#36381) …
Added UniqueFactorizationMonoid.finprod_pow_count_eq_of_subsingleton_unitsView on Github →