Namespace `Multiset` 2 theorems

Rigidity of the products prod(1-zⁿ) Multiset.filter_ne_zero_eq_of_forall_prod_one_sub_pow_eq 0 below · cited by 2 · depth 23
Elementary symmetric functions modulo powers of an ideal Multiset.esymm_map_sub_esymm_map_mem_pow_succ 0 below · cited by 1 · depth 32

Documents the Lean sources in this repository (Lean v4.33.1, Mathlib v4.33.0). Statements are quoted textually from the .lean files; dependency edges are the import Theorems.Thm_… lines of the proof modules. About these pages.

Namespace Multiset 2 theorems

Namespace `Multiset` 2 theorems