Re: Union of two subgroups
Victor Makarov <[email protected]> Tue, 17 Nov 2020 22:13:46 -0500
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <CAHZyMifLCeaA-FYamk3-GNCmtBA9r6PwbLHu2SvVOrJ-5+qt7A@mail.gmail.com> |
Thanks, I'll check them out. On Tue, Nov 17, 2020 at 7:51 AM Adam Naumowicz <[email protected]> wrote: > Dear Victor, > > On Mon, 16 Nov 2020, Victor Makarov wrote: > > > Dear All: > > > > I cannot find in MML a theorem that the union of two subgroups is a > > subgroup iff one of the subgroups is a subset of the other subgroup. > > > > The same question about the product of two subgroups H and K: > > > > H*K is a subgroup iff H*K = K*H. > > This may not be exactly what you want, but have you checked these > theorems: > > theorem :: GROUP_4:50 > H1 "\/" H2 = gr(H1 * H2); > > theorem :: GROUP_4:51 > H1 * H2 = H2 * H1 implies the carrier of H1 "\/" H2 = H1 * H2; > > ? > > Best regards, > > Adam Naumowicz > > =========================================================================== > Division of Programming and Formal Methods Fax: +48(85)738-83-33 > Institute of Computer Science Tel: +48(85)738-83-06 (office) > University of Bialystok E-mail: [email protected] > Ciolkowskiego 1M, 15-245 Bialystok, Poland > http://math.uwb.edu.pl/~adamn/ > =========================================================================== > >