Theorem Set.powersetCard.nontrivial'

Modification history

2026-02-12 04:48

Mathlib/Data/Set/PowersetCard.lean

chore: separate basic API for `Set.powersetCard` (#35068) …

Modified Set.powersetCard.nontrivial'View on Github →

2026-01-29 18:04

Mathlib/GroupTheory/GroupAction/SubMulAction/Combination.lean

chore(GroupTheory/GroupAction/SubMulAction/Combination.lean): rename Nat.Combination to Set.powersetCard (#34581) …

Added Set.powersetCard.nontrivial'View on Github →