OAI/GroupTheory/PolycyclicRecognition/Algebra/CommutingSubgroupProduct.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Products of commuting nilpotent subgroups

Multiplication is a surjective homomorphism from the direct product onto the join when the two subgroups centralize each other. Nilpotence passes through this explicit homomorphism.

  1. def OAI.PolycyclicRecognition.commutingProductHom line 18
  2. theorem OAI.PolycyclicRecognition.commutingProductHom_range line 29
  3. theorem OAI.PolycyclicRecognition.nilpotent_sup_of_commute line 42