Theorems · Theorem · combinatorics

Finset.mk.congr_simp

∀ {α : Type u_4} (val val_1 : Multiset α) (e_val : val = val_1) (nodup : val.Nodup),
  { val := val, nodup := nodup } = { val := val_1, nodup := ⋯ }

Defined in

Mathlib.Data.Finset.Defs

Cited by

6 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Quot.sound