Commit 2025-03-12 13:47 78845f66

View on Github →

feat: density of a union of finsets (#22629) From PlainCombi (LeanCamCombi)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Field.lean

added theorem Finset.dens_biUnion

added theorem Finset.dens_biUnion_le

added theorem Finset.dens_disjiUnion

added theorem Finset.dens_eq_sum_dens_fiberwise

added theorem Finset.dens_eq_sum_dens_image

Modified Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

modified theorem Finset.card_biUnion

Modified Mathlib/Combinatorics/Enumerative/Catalan.lean

Modified Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

Modified Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean

Modified Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean

Modified Mathlib/GroupTheory/OrderOfElement.lean

Modified Mathlib/NumberTheory/NumberField/Embeddings.lean

Modified Mathlib/Order/Partition/Finpartition.lean