Theorem Nat.Combination.nontrivial'

Modification history

2026-01-29 18:04
Mathlib/GroupTheory/GroupAction/SubMulAction/Combination.lean
chore(GroupTheory/GroupAction/SubMulAction/Combination.lean): rename Nat.Combination to Set.powersetCard (#34581) …
Deleted Nat.Combination.nontrivial'View on Github →
2025-12-01 10:02
Mathlib/GroupTheory/GroupAction/SubMulAction/Combination.lean
feat(GroupTheory/GroupAction/SubMulAction/Combination): combinations and group actions (#27107) …
Added Nat.Combination.nontrivial'View on Github →