chore(group_theory/submonoid): split into 3 files (#3058)

Now * `group_theory.submonoid.basic` contains the definition, `complete_lattice` structure, and some basic facts about `closure`; * `group_theory.submonoid.operations` contains definitions of various operations on submonoids; * `group_theory.submonoid.membership` contains various facts about membership in a submonoid or the submonoid closure of a set.
leanprover-community · Jun 28, 2020 · 2ec83dc · 2ec83dc
1 parent 4ad82e5
commit 2ec83dc
Show file tree

Hide file tree

Showing 7 changed files with 997 additions and 823 deletions.
diff --git a/src/group_theory/subgroup.lean b/src/group_theory/subgroup.lean
@@ -817,8 +817,8 @@ open set
 
 lemma gsmul_mem (H : add_subgroup A) {x : A} (hx : x ∈ H) :
   ∀ n : ℤ, gsmul n x ∈ H
-| (int.of_nat n) := add_submonoid.smul_mem H.to_add_submonoid hx n
-| -[1+ n]        := H.neg_mem' $ H.add_mem hx $ add_submonoid.smul_mem H.to_add_submonoid hx n
+| (int.of_nat n) := add_submonoid.nsmul_mem H.to_add_submonoid hx n
+| -[1+ n]        := H.neg_mem' $ H.add_mem hx $ add_submonoid.nsmul_mem H.to_add_submonoid hx n
 
 lemma sub_mem (H : add_subgroup A) {x y : A} (hx : x ∈ H) (hy : y ∈ H) : x - y ∈ H :=
 H.add_mem hx (H.neg_mem hy)