Theorem Multiset.one_le_prod_map

Modification history

2026-02-16 07:36
Mathlib/Algebra/Order/BigOperators/GroupWithZero/Multiset.lean
feat(NumberTheory/Height/Basic): add bounds for sums (#34330) …
Added Multiset.one_le_prod_mapView on Github →