Commit 2023-01-14 04:26 ef7866bd

View on Github →

feat: port GroupTheory.GroupAction.Support (#1560)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/GroupAction/Support.lean

added theorem MulAction.Supports.mono

added theorem MulAction.Supports.smul

added def MulAction.Supports

added theorem MulAction.supports_of_mem