Def Nat.Combination.mulActionHom_of_embedding

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.mulActionHom_of_embedding 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.mulActionHom_of_embedding View on Github →