Skip to content

Commit b29921c

Browse files
Ruben-VandeVeldeRuben-VandeVelde
committed
feat: port Algebra.Modeq (#3921)
1 parent 0b1f387 commit b29921c

File tree

3 files changed

+346
-1
lines changed

3 files changed

+346
-1
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -163,6 +163,7 @@ import Mathlib.Algebra.Lie.Basic
163163
import Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra
164164
import Mathlib.Algebra.Lie.Subalgebra
165165
import Mathlib.Algebra.LinearRecurrence
166+
import Mathlib.Algebra.ModEq
166167
import Mathlib.Algebra.Module.Algebra
167168
import Mathlib.Algebra.Module.Basic
168169
import Mathlib.Algebra.Module.BigOperators

‎Mathlib/Algebra/GroupPower/Lemmas.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -580,7 +580,8 @@ theorem mul_bit1 [NonAssocRing R] {n r : R} : r * bit1 n = (2 : ℤ) • (r * n)
580580
end bit0_bit1
581581

582582
/-- Note this holds in marginally more generality than `Int.cast_mul` -/
583-
theorem Int.cast_mul_eq_zsmul_cast [AddCommGroupWithOne α] : ∀ m n, ((m * n : ℤ) : α) = m • n :=
583+
theorem Int.cast_mul_eq_zsmul_cast [AddCommGroupWithOne α] :
584+
∀ m n, ((m * n : ℤ) : α) = m • (n : α) :=
584585
fun m =>
585586
Int.inductionOn' m 0 (by simp) (fun k _ ih n => by simp [add_mul, add_zsmul, ih]) fun k _ ih n =>
586587
by simp [sub_mul, sub_zsmul, ih, ← sub_eq_add_neg]

‎Mathlib/Algebra/ModEq.lean‎

Lines changed: 343 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,343 @@
1+
/-
2+
Copyright (c) 2023 Yaël Dillies. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Yaël Dillies
5+
6+
! This file was ported from Lean 3 source module algebra.modeq
7+
! leanprover-community/mathlib commit a07d750983b94c530ab69a726862c2ab6802b38c
8+
! Please do not edit these lines, except to modify the commit id
9+
! if you have ported upstream changes.
10+
-/
11+
import Mathlib.Data.Int.ModEq
12+
import Mathlib.GroupTheory.QuotientGroup
13+
14+
/-!
15+
# Equality modulo an element
16+
17+
This file defines equality modulo an element in a commutative group.
18+
19+
## Main definitions
20+
21+
* `a ≡ b [PMOD p]`: `a` and `b` are congruent modulo a`p`.
22+
23+
## See also
24+
25+
`SModEq` is a generalisation to arbitrary submodules.
26+
27+
## TODO
28+
29+
Delete `Int.ModEq` in favour of `AddCommGroup.ModEq`. Generalise `SModEq` to `AddSubgroup` and
30+
redefine `AddCommGroup.ModEq` using it. Once this is done, we can rename `AddCommGroup.ModEq`
31+
to `AddSubgroup.ModEq` and multiplicativise it. Longer term, we could generalise to submonoids and
32+
also unify with `Nat.ModEq`.
33+
-/
34+
35+
36+
namespace AddCommGroup
37+
38+
variable {α : Type _}
39+
40+
section AddCommGroup
41+
42+
variable [AddCommGroup α] {p a a₁ a₂ b b₁ b₂ c : α} {n : ℕ} {z : ℤ}
43+
44+
/-- `a ≡ b [PMOD p]` means that `b` is congruent to `a` modulo `p`.
45+
46+
Equivalently (as shown in `Algebra.Order.ToIntervalMod`), `b` does not lie in the open interval
47+
`(a, a + p)` modulo `p`, or `toIcoMod hp a` disagrees with `toIocMod hp a` at `b`, or
48+
`toIcoDiv hp a` disagrees with `toIocDiv hp a` at `b`. -/
49+
def ModEq (p a b : α) : Prop :=
50+
∃ z : ℤ, b - a = z • p
51+
#align add_comm_group.modeq AddCommGroup.ModEq
52+
53+
notation:50 a " ≡ " b " [PMOD " p "]" => ModEq p a b
54+
55+
@[refl, simp]
56+
theorem modEq_refl (a : α) : a ≡ a [PMOD p] :=
57+
⟨0, by simp⟩
58+
#align add_comm_group.modeq_refl AddCommGroup.modEq_refl
59+
60+
theorem modEq_rfl : a ≡ a [PMOD p] :=
61+
modEq_refl _
62+
#align add_comm_group.modeq_rfl AddCommGroup.modEq_rfl
63+
64+
theorem modEq_comm : a ≡ b [PMOD p] ↔ b ≡ a [PMOD p] :=
65+
(Equiv.neg _).exists_congr_left.trans <| by simp [ModEq, ← neg_eq_iff_eq_neg]
66+
#align add_comm_group.modeq_comm AddCommGroup.modEq_comm
67+
68+
alias modEq_comm ↔ ModEq.symm _
69+
#align add_comm_group.modeq.symm AddCommGroup.ModEq.symm
70+
71+
attribute [symm] ModEq.symm
72+
73+
@[trans]
74+
theorem ModEq.trans : a ≡ b [PMOD p] → b ≡ c [PMOD p] → a ≡ c [PMOD p] := fun ⟨m, hm⟩ ⟨n, hn⟩ =>
75+
⟨m + n, by simp [add_smul, ← hm, ← hn]⟩
76+
#align add_comm_group.modeq.trans AddCommGroup.ModEq.trans
77+
78+
instance : IsRefl _ (ModEq p) :=
79+
⟨modEq_refl⟩
80+
81+
@[simp]
82+
theorem neg_modEq_neg : -a ≡ -b [PMOD p] ↔ a ≡ b [PMOD p] :=
83+
modEq_comm.trans <| by simp [ModEq, neg_add_eq_sub]
84+
#align add_comm_group.neg_modeq_neg AddCommGroup.neg_modEq_neg
85+
86+
alias neg_modEq_neg ↔ ModEq.of_neg ModEq.neg
87+
#align add_comm_group.modeq.of_neg AddCommGroup.ModEq.of_neg
88+
#align add_comm_group.modeq.neg AddCommGroup.ModEq.neg
89+
90+
@[simp]
91+
theorem modEq_neg : a ≡ b [PMOD -p] ↔ a ≡ b [PMOD p] :=
92+
modEq_comm.trans <| by simp [ModEq, ← neg_eq_iff_eq_neg]
93+
#align add_comm_group.modeq_neg AddCommGroup.modEq_neg
94+
95+
alias modEq_neg ↔ ModEq.of_neg' ModEq.neg'
96+
#align add_comm_group.modeq.of_neg' AddCommGroup.ModEq.of_neg'
97+
#align add_comm_group.modeq.neg' AddCommGroup.ModEq.neg'
98+
99+
theorem modEq_sub (a b : α) : a ≡ b [PMOD b - a] :=
100+
⟨1, (one_smul _ _).symm⟩
101+
#align add_comm_group.modeq_sub AddCommGroup.modEq_sub
102+
103+
@[simp]
104+
theorem modEq_zero : a ≡ b [PMOD 0] ↔ a = b := by simp [ModEq, sub_eq_zero, eq_comm]
105+
#align add_comm_group.modeq_zero AddCommGroup.modEq_zero
106+
107+
@[simp]
108+
theorem self_modEq_zero : p ≡ 0 [PMOD p] :=
109+
⟨-1, by simp⟩
110+
#align add_comm_group.self_modeq_zero AddCommGroup.self_modEq_zero
111+
112+
@[simp]
113+
theorem zsmul_modEq_zero (z : ℤ) : z • p ≡ 0 [PMOD p] :=
114+
⟨-z, by simp⟩
115+
#align add_comm_group.zsmul_modeq_zero AddCommGroup.zsmul_modEq_zero
116+
117+
theorem add_zsmul_modEq (z : ℤ) : a + z • p ≡ a [PMOD p] :=
118+
⟨-z, by simp⟩
119+
#align add_comm_group.add_zsmul_modeq AddCommGroup.add_zsmul_modEq
120+
121+
theorem zsmul_add_modEq (z : ℤ) : z • p + a ≡ a [PMOD p] :=
122+
⟨-z, by simp [← sub_sub]⟩
123+
#align add_comm_group.zsmul_add_modeq AddCommGroup.zsmul_add_modEq
124+
125+
theorem add_nsmul_modEq (n : ℕ) : a + n • p ≡ a [PMOD p] :=
126+
⟨-n, by simp⟩
127+
#align add_comm_group.add_nsmul_modeq AddCommGroup.add_nsmul_modEq
128+
129+
theorem nsmul_add_modEq (n : ℕ) : n • p + a ≡ a [PMOD p] :=
130+
⟨-n, by simp [← sub_sub]⟩
131+
#align add_comm_group.nsmul_add_modeq AddCommGroup.nsmul_add_modEq
132+
133+
namespace ModEq
134+
135+
protected theorem add_zsmul (z : ℤ) : a ≡ b [PMOD p] → a + z • p ≡ b [PMOD p] :=
136+
(add_zsmul_modEq _).trans
137+
#align add_comm_group.modeq.add_zsmul AddCommGroup.ModEq.add_zsmul
138+
139+
protected theorem zsmul_add (z : ℤ) : a ≡ b [PMOD p] → z • p + a ≡ b [PMOD p] :=
140+
(zsmul_add_modEq _).trans
141+
#align add_comm_group.modeq.zsmul_add AddCommGroup.ModEq.zsmul_add
142+
143+
protected theorem add_nsmul (n : ℕ) : a ≡ b [PMOD p] → a + n • p ≡ b [PMOD p] :=
144+
(add_nsmul_modEq _).trans
145+
#align add_comm_group.modeq.add_nsmul AddCommGroup.ModEq.add_nsmul
146+
147+
protected theorem nsmul_add (n : ℕ) : a ≡ b [PMOD p] → n • p + a ≡ b [PMOD p] :=
148+
(nsmul_add_modEq _).trans
149+
#align add_comm_group.modeq.nsmul_add AddCommGroup.ModEq.nsmul_add
150+
151+
protected theorem of_zsmul : a ≡ b [PMOD z • p] → a ≡ b [PMOD p] := fun ⟨m, hm⟩ =>
152+
⟨m * z, by rwa [mul_smul]⟩
153+
#align add_comm_group.modeq.of_zsmul AddCommGroup.ModEq.of_zsmul
154+
155+
protected theorem of_nsmul : a ≡ b [PMOD n • p] → a ≡ b [PMOD p] := fun ⟨m, hm⟩ =>
156+
⟨m * n, by rwa [mul_smul, coe_nat_zsmul]⟩
157+
#align add_comm_group.modeq.of_nsmul AddCommGroup.ModEq.of_nsmul
158+
159+
protected theorem zsmul : a ≡ b [PMOD p] → z • a ≡ z • b [PMOD z • p] :=
160+
Exists.imp fun m hm => by rw [← smul_sub, hm, smul_comm]
161+
#align add_comm_group.modeq.zsmul AddCommGroup.ModEq.zsmul
162+
163+
protected theorem nsmul : a ≡ b [PMOD p] → n • a ≡ n • b [PMOD n • p] :=
164+
Exists.imp fun m hm => by rw [← smul_sub, hm, smul_comm]
165+
#align add_comm_group.modeq.nsmul AddCommGroup.ModEq.nsmul
166+
167+
end ModEq
168+
169+
@[simp]
170+
theorem zsmul_modEq_zsmul [NoZeroSMulDivisors ℤ α] (hn : z ≠ 0) :
171+
z • a ≡ z • b [PMOD z • p] ↔ a ≡ b [PMOD p] :=
172+
exists_congr fun m => by rw [← smul_sub, smul_comm, smul_right_inj hn]
173+
#align add_comm_group.zsmul_modeq_zsmul AddCommGroup.zsmul_modEq_zsmul
174+
175+
@[simp]
176+
theorem nsmul_modEq_nsmul [NoZeroSMulDivisors ℕ α] (hn : n ≠ 0) :
177+
n • a ≡ n • b [PMOD n • p] ↔ a ≡ b [PMOD p] :=
178+
exists_congr fun m => by rw [← smul_sub, smul_comm, smul_right_inj hn]
179+
#align add_comm_group.nsmul_modeq_nsmul AddCommGroup.nsmul_modEq_nsmul
180+
181+
alias zsmul_modEq_zsmul ↔ ModEq.zsmul_cancel _
182+
#align add_comm_group.modeq.zsmul_cancel AddCommGroup.ModEq.zsmul_cancel
183+
184+
alias nsmul_modEq_nsmul ↔ ModEq.nsmul_cancel _
185+
#align add_comm_group.modeq.nsmul_cancel AddCommGroup.ModEq.nsmul_cancel
186+
187+
namespace ModEq
188+
189+
@[simp]
190+
protected theorem add_iff_left :
191+
a₁ ≡ b₁ [PMOD p] → (a₁ + a₂ ≡ b₁ + b₂ [PMOD p] ↔ a₂ ≡ b₂ [PMOD p]) := fun ⟨m, hm⟩ =>
192+
(Equiv.addLeft m).symm.exists_congr_left.trans <| by simp [add_sub_add_comm, hm, add_smul, ModEq]
193+
#align add_comm_group.modeq.add_iff_left AddCommGroup.ModEq.add_iff_left
194+
195+
@[simp]
196+
protected theorem add_iff_right :
197+
a₂ ≡ b₂ [PMOD p] → (a₁ + a₂ ≡ b₁ + b₂ [PMOD p] ↔ a₁ ≡ b₁ [PMOD p]) := fun ⟨m, hm⟩ =>
198+
(Equiv.addRight m).symm.exists_congr_left.trans <| by simp [add_sub_add_comm, hm, add_smul, ModEq]
199+
#align add_comm_group.modeq.add_iff_right AddCommGroup.ModEq.add_iff_right
200+
201+
@[simp]
202+
protected theorem sub_iff_left :
203+
a₁ ≡ b₁ [PMOD p] → (a₁ - a₂ ≡ b₁ - b₂ [PMOD p] ↔ a₂ ≡ b₂ [PMOD p]) := fun ⟨m, hm⟩ =>
204+
(Equiv.subLeft m).symm.exists_congr_left.trans <| by simp [sub_sub_sub_comm, hm, sub_smul, ModEq]
205+
#align add_comm_group.modeq.sub_iff_left AddCommGroup.ModEq.sub_iff_left
206+
207+
@[simp]
208+
protected theorem sub_iff_right :
209+
a₂ ≡ b₂ [PMOD p] → (a₁ - a₂ ≡ b₁ - b₂ [PMOD p] ↔ a₁ ≡ b₁ [PMOD p]) := fun ⟨m, hm⟩ =>
210+
(Equiv.subRight m).symm.exists_congr_left.trans <| by simp [sub_sub_sub_comm, hm, sub_smul, ModEq]
211+
#align add_comm_group.modeq.sub_iff_right AddCommGroup.ModEq.sub_iff_right
212+
213+
alias ModEq.add_iff_left ↔ add_left_cancel add
214+
#align add_comm_group.modeq.add_left_cancel AddCommGroup.ModEq.add_left_cancel
215+
#align add_comm_group.modeq.add AddCommGroup.ModEq.add
216+
217+
alias ModEq.add_iff_right ↔ add_right_cancel _
218+
#align add_comm_group.modeq.add_right_cancel AddCommGroup.ModEq.add_right_cancel
219+
220+
alias ModEq.sub_iff_left ↔ sub_left_cancel sub
221+
#align add_comm_group.modeq.sub_left_cancel AddCommGroup.ModEq.sub_left_cancel
222+
#align add_comm_group.modeq.sub AddCommGroup.ModEq.sub
223+
224+
alias ModEq.sub_iff_right ↔ sub_right_cancel _
225+
#align add_comm_group.modeq.sub_right_cancel AddCommGroup.ModEq.sub_right_cancel
226+
227+
-- porting note: doesn't work
228+
-- attribute [protected] add_left_cancel add_right_cancel add sub_left_cancel sub_right_cancel sub
229+
230+
protected theorem add_left (c : α) (h : a ≡ b [PMOD p]) : c + a ≡ c + b [PMOD p] :=
231+
modEq_rfl.add h
232+
#align add_comm_group.modeq.add_left AddCommGroup.ModEq.add_left
233+
234+
protected theorem sub_left (c : α) (h : a ≡ b [PMOD p]) : c - a ≡ c - b [PMOD p] :=
235+
modEq_rfl.sub h
236+
#align add_comm_group.modeq.sub_left AddCommGroup.ModEq.sub_left
237+
238+
protected theorem add_right (c : α) (h : a ≡ b [PMOD p]) : a + c ≡ b + c [PMOD p] :=
239+
h.add modEq_rfl
240+
#align add_comm_group.modeq.add_right AddCommGroup.ModEq.add_right
241+
242+
protected theorem sub_right (c : α) (h : a ≡ b [PMOD p]) : a - c ≡ b - c [PMOD p] :=
243+
h.sub modEq_rfl
244+
#align add_comm_group.modeq.sub_right AddCommGroup.ModEq.sub_right
245+
246+
protected theorem add_left_cancel' (c : α) : c + a ≡ c + b [PMOD p] → a ≡ b [PMOD p] :=
247+
modEq_rfl.add_left_cancel
248+
#align add_comm_group.modeq.add_left_cancel' AddCommGroup.ModEq.add_left_cancel'
249+
250+
protected theorem add_right_cancel' (c : α) : a + c ≡ b + c [PMOD p] → a ≡ b [PMOD p] :=
251+
modEq_rfl.add_right_cancel
252+
#align add_comm_group.modeq.add_right_cancel' AddCommGroup.ModEq.add_right_cancel'
253+
254+
protected theorem sub_left_cancel' (c : α) : c - a ≡ c - b [PMOD p] → a ≡ b [PMOD p] :=
255+
modEq_rfl.sub_left_cancel
256+
#align add_comm_group.modeq.sub_left_cancel' AddCommGroup.ModEq.sub_left_cancel'
257+
258+
protected theorem sub_right_cancel' (c : α) : a - c ≡ b - c [PMOD p] → a ≡ b [PMOD p] :=
259+
modEq_rfl.sub_right_cancel
260+
#align add_comm_group.modeq.sub_right_cancel' AddCommGroup.ModEq.sub_right_cancel'
261+
262+
end ModEq
263+
264+
theorem modEq_sub_iff_add_modEq' : a ≡ b - c [PMOD p] ↔ c + a ≡ b [PMOD p] := by
265+
simp [ModEq, sub_sub]
266+
#align add_comm_group.modeq_sub_iff_add_modeq' AddCommGroup.modEq_sub_iff_add_modEq'
267+
268+
theorem modEq_sub_iff_add_modEq : a ≡ b - c [PMOD p] ↔ a + c ≡ b [PMOD p] :=
269+
modEq_sub_iff_add_modEq'.trans <| by rw [add_comm]
270+
#align add_comm_group.modeq_sub_iff_add_modeq AddCommGroup.modEq_sub_iff_add_modEq
271+
272+
theorem sub_modEq_iff_modEq_add' : a - b ≡ c [PMOD p] ↔ a ≡ b + c [PMOD p] :=
273+
modEq_comm.trans <| modEq_sub_iff_add_modEq'.trans modEq_comm
274+
#align add_comm_group.sub_modeq_iff_modeq_add' AddCommGroup.sub_modEq_iff_modEq_add'
275+
276+
theorem sub_modEq_iff_modEq_add : a - b ≡ c [PMOD p] ↔ a ≡ c + b [PMOD p] :=
277+
modEq_comm.trans <| modEq_sub_iff_add_modEq.trans modEq_comm
278+
#align add_comm_group.sub_modeq_iff_modeq_add AddCommGroup.sub_modEq_iff_modEq_add
279+
280+
@[simp]
281+
theorem sub_modEq_zero : a - b ≡ 0 [PMOD p] ↔ a ≡ b [PMOD p] := by simp [sub_modEq_iff_modEq_add]
282+
#align add_comm_group.sub_modeq_zero AddCommGroup.sub_modEq_zero
283+
284+
@[simp]
285+
theorem add_modEq_left : a + b ≡ a [PMOD p] ↔ b ≡ 0 [PMOD p] := by simp [← modEq_sub_iff_add_modEq']
286+
#align add_comm_group.add_modeq_left AddCommGroup.add_modEq_left
287+
288+
@[simp]
289+
theorem add_modEq_right : a + b ≡ b [PMOD p] ↔ a ≡ 0 [PMOD p] := by simp [← modEq_sub_iff_add_modEq]
290+
#align add_comm_group.add_modeq_right AddCommGroup.add_modEq_right
291+
292+
theorem modEq_iff_eq_add_zsmul : a ≡ b [PMOD p] ↔ ∃ z : ℤ, b = a + z • p := by
293+
simp_rw [ModEq, sub_eq_iff_eq_add']
294+
#align add_comm_group.modeq_iff_eq_add_zsmul AddCommGroup.modEq_iff_eq_add_zsmul
295+
296+
theorem not_modEq_iff_ne_add_zsmul : ¬a ≡ b [PMOD p] ↔ ∀ z : ℤ, b ≠ a + z • p := by
297+
rw [modEq_iff_eq_add_zsmul, not_exists]
298+
#align add_comm_group.not_modeq_iff_ne_add_zsmul AddCommGroup.not_modEq_iff_ne_add_zsmul
299+
300+
theorem modEq_iff_eq_mod_zmultiples : a ≡ b [PMOD p] ↔ (b : α ⧸ AddSubgroup.zmultiples p) = a := by
301+
simp_rw [modEq_iff_eq_add_zsmul, QuotientAddGroup.eq_iff_sub_mem, AddSubgroup.mem_zmultiples_iff,
302+
eq_sub_iff_add_eq', eq_comm]
303+
#align add_comm_group.modeq_iff_eq_mod_zmultiples AddCommGroup.modEq_iff_eq_mod_zmultiples
304+
305+
theorem not_modEq_iff_ne_mod_zmultiples :
306+
¬a ≡ b [PMOD p] ↔ (b : α ⧸ AddSubgroup.zmultiples p) ≠ a :=
307+
modEq_iff_eq_mod_zmultiples.not
308+
#align add_comm_group.not_modeq_iff_ne_mod_zmultiples AddCommGroup.not_modEq_iff_ne_mod_zmultiples
309+
310+
end AddCommGroup
311+
312+
@[simp]
313+
theorem modEq_iff_int_modEq {a b z : ℤ} : a ≡ b [PMOD z] ↔ a ≡ b [ZMOD z] := by
314+
simp [ModEq, dvd_iff_exists_eq_mul_left, Int.modEq_iff_dvd]
315+
#align add_comm_group.modeq_iff_int_modeq AddCommGroup.modEq_iff_int_modEq
316+
317+
section AddCommGroupWithOne
318+
319+
variable [AddCommGroupWithOne α] [CharZero α]
320+
321+
@[simp, norm_cast]
322+
theorem int_cast_modEq_int_cast {a b z : ℤ} : a ≡ b [PMOD (z : α)] ↔ a ≡ b [PMOD z] := by
323+
simp_rw [ModEq, ← Int.cast_mul_eq_zsmul_cast]
324+
norm_cast
325+
#align add_comm_group.int_cast_modeq_int_cast AddCommGroup.int_cast_modEq_int_cast
326+
327+
@[simp, norm_cast]
328+
theorem nat_cast_modEq_nat_cast {a b n : ℕ} : a ≡ b [PMOD (n : α)] ↔ a ≡ b [MOD n] := by
329+
simp_rw [← Int.coe_nat_modEq_iff, ← modEq_iff_int_modEq, ← @int_cast_modEq_int_cast α,
330+
Int.cast_ofNat]
331+
#align add_comm_group.nat_cast_modeq_nat_cast AddCommGroup.nat_cast_modEq_nat_cast
332+
333+
alias int_cast_modEq_int_cast ↔ ModEq.of_int_cast ModEq.int_cast
334+
#align add_comm_group.modeq.of_int_cast AddCommGroup.ModEq.of_int_cast
335+
#align add_comm_group.modeq.int_cast AddCommGroup.ModEq.int_cast
336+
337+
alias nat_cast_modEq_nat_cast ↔ _root_.Nat.ModEq.of_nat_cast ModEq.nat_cast
338+
#align nat.modeq.of_nat_cast Nat.ModEq.of_nat_cast
339+
#align add_comm_group.modeq.nat_cast AddCommGroup.ModEq.nat_cast
340+
341+
end AddCommGroupWithOne
342+
343+
end AddCommGroup

0 commit comments

Comments
 (0)