Commit 2026-01-29 18:04 c5afc4c6

View on Github →

chore(GroupTheory/GroupAction/SubMulAction/Combination.lean): rename Nat.Combination to Set.powersetCard (#34581) Following suggestion by @ocfnash and @alreadydone , rename Nat.Combination as Set.powersetCard, in analogy to Finset.powerset and Finset.powersetCard. Some later improvements are given in #34307

Estimated changes

Modified Mathlib/GroupTheory/GroupAction/SubMulAction/Combination.lean

deleted theorem Nat.Combination.addAction_faithful

deleted theorem Nat.Combination.coe_coe

deleted theorem Nat.Combination.coe_compl

deleted theorem Nat.Combination.coe_mulActionHom_of_embedding

deleted theorem Nat.Combination.coe_smul

deleted def Nat.Combination.compl

deleted theorem Nat.Combination.compl_bijective

deleted theorem Nat.Combination.compl_compl

deleted theorem Nat.Combination.eq_iff_subset

deleted theorem Nat.Combination.exists_mem_notMem

deleted theorem Nat.Combination.faithfulSMul

deleted theorem Nat.Combination.faithfulVAdd

deleted theorem Nat.Combination.isPretransitive

deleted theorem Nat.Combination.isPretransitive_of_isMultiplyPretransitive

deleted theorem Nat.Combination.mem_coe_iff

deleted theorem Nat.Combination.mem_compl

deleted theorem Nat.Combination.mem_iff

deleted def Nat.Combination.mulActionHom_of_embedding

deleted theorem Nat.Combination.mulActionHom_of_embedding_surjective

deleted def Nat.Combination.mulActionHom_singleton

deleted theorem Nat.Combination.mulActionHom_singleton_bijective

deleted theorem Nat.Combination.mulAction_faithful

deleted theorem Nat.Combination.nontrivial'

deleted theorem Nat.Combination.nontrivial

deleted def Nat.Combination.subMulAction

deleted def Nat.Combination

added theorem Set.powersetCard.addAction_faithful

added theorem Set.powersetCard.coe_coe

added theorem Set.powersetCard.coe_compl

added theorem Set.powersetCard.coe_mulActionHom_of_embedding

added theorem Set.powersetCard.coe_smul

added def Set.powersetCard.compl

added theorem Set.powersetCard.compl_bijective

added theorem Set.powersetCard.compl_compl

added theorem Set.powersetCard.eq_iff_subset

added theorem Set.powersetCard.exists_mem_notMem

added theorem Set.powersetCard.faithfulSMul

added theorem Set.powersetCard.faithfulVAdd

added theorem Set.powersetCard.isPretransitive

added theorem Set.powersetCard.isPretransitive_of_isMultiplyPretransitive

added theorem Set.powersetCard.mem_coe_iff

added theorem Set.powersetCard.mem_compl

added theorem Set.powersetCard.mem_iff

added def Set.powersetCard.mulActionHom_of_embedding

added theorem Set.powersetCard.mulActionHom_of_embedding_surjective

added def Set.powersetCard.mulActionHom_singleton

added theorem Set.powersetCard.mulActionHom_singleton_bijective

added theorem Set.powersetCard.mulAction_faithful

added theorem Set.powersetCard.nontrivial'

added theorem Set.powersetCard.nontrivial

added def Set.powersetCard.subMulAction

added def Set.powersetCard