Theorem SubMulAction.Enat_card_ofStabilizer_eq_add_one

Modification history

2025-05-20 07:44

Mathlib/GroupTheory/GroupAction/SubMulAction/OfStabilizer.lean

feat(GroupTheory.GroupAction.SubMulAction.OfStabilizer) : action of stabilizer on complement of a point (#23962) …

Added SubMulAction.Enat_card_ofStabilizer_eq_add_one View on Github →