Talk:Internal Direct Product Theorem

Why do we have both https://proofwiki.org/wiki/Internal_Direct_Product_Theorem and https://proofwiki.org/wiki/Definition:Internal_Group_Direct_Product ? Why can't we just have a 3rd definition? BCLC (talk) 01:11, 28 October 2021 (UTC)

The short answer is because it is introduced in the published works that we have available as an iff proof and not as an equivalent definition.

We try to ensure that we introduce such equivalences as formal definitions only when it is documented as such in the literature.

The thinking is that while an equivalence may be straightforward to formulate, its subsequent use as a definition may be dubious.

Hence, if an author does consider such an equivalence useful as a definition, then we will follow that lead and include such in our database as a definition.

Otherwise we may find ourselves overburdened with a large number of definitions, which becomes unwieldy to maintain.

There are already cases where there are large number of definitions (in this context "large" means "over four") -- examples being: Definition:Normal Subgroup, Definition:Prime Number, Definition:Injection.

No need to add greater complexity where it is unwarranted. --prime mover (talk) 19:44, 22 March 2022 (UTC)