Commit 2023-01-30 08:08 2b13f3b2

View on Github →

feat: port GroupTheory.GroupAction.SubMulAction.Pointwise (#1893)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/GroupAction/SubMulAction/Pointwise.lean

added theorem SubMulAction.coe_mul

added theorem SubMulAction.coe_one

added theorem SubMulAction.coe_pow

added theorem SubMulAction.mem_mul

added theorem SubMulAction.mem_one

added theorem SubMulAction.subset_coe_one

added theorem SubMulAction.subset_coe_pow