Commit 2023-11-14 03:24 86eae0cb

View on Github →

feat: Simple Subgroup lemmas (#8341)

Estimated changes

Modified Mathlib/GroupTheory/Subgroup/Actions.lean

added theorem Subgroup.mk_smul

modified theorem Subgroup.smul_def

Modified Mathlib/GroupTheory/Subgroup/Basic.lean

modified theorem Subgroup.closure_eq_bot_iff

added theorem Subgroup.nonempty

Modified Mathlib/GroupTheory/Submonoid/Operations.lean

added theorem Submonoid.mk_smul

modified theorem Submonoid.smul_def