Commit 2023-01-27 14:47 283f67f9

View on Github →

feat: port GroupTheory.GroupAction.SubMulAction (#1872)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/GroupAction/SubMulAction.lean

added theorem SetLike.forall_smul_mem_iff

added theorem SetLike.mk_smul_mk

added theorem SetLike.smul_def

added theorem SubMulAction.coe_copy

added theorem SubMulAction.copy_eq

added theorem SubMulAction.ext

added theorem SubMulAction.mem_carrier

added theorem SubMulAction.neg_mem

added theorem SubMulAction.neg_mem_iff

added theorem SubMulAction.smul_mem

added theorem SubMulAction.smul_mem_iff'

added theorem SubMulAction.smul_mem_iff

added theorem SubMulAction.smul_of_tower_mem

added theorem SubMulAction.stabilizer_of_subMul.submonoid

added theorem SubMulAction.stabilizer_of_subMul

added theorem SubMulAction.subtype_apply

added theorem SubMulAction.subtype_eq_val

added theorem SubMulAction.val_image_orbit

added theorem SubMulAction.val_neg

added theorem SubMulAction.val_smul

added theorem SubMulAction.val_smul_of_tower

added theorem SubMulAction.zero_mem

added structure SubMulAction