Code

more on commutator subgroups#2205

Code

Open

Alizter wants to merge 7 commits intoHoTT:masterHoTT/Coq-HoTT:masterfrom Alizter:ps/rr/more_on_commutator_subgroupsAlizter/HoTT:ps/rr/more_on_commutator_subgroupsCopy head branch name to clipboard

+346-39

Commits

Commits on Feb 9, 2025

• more on commutator subgroups

  Show description for 1c7dd19
  Alizter

  committed
  1c7dd19

  Copy full SHA for 1c7dd19

• introduce opposite group and use it to shorten proofs

  Show description for eb714a6
  Alizter

  committed
  eb714a6

  Copy full SHA for eb714a6

• commutator of subgroups is symmetric

  Show description for fe6aca5
  Alizter

  committed
  fe6aca5

  Copy full SHA for fe6aca5

• shorten argument in isnormal_subgroup_commutator

  Show description for 3ea6703
  Alizter

  committed
  3ea6703

  Copy full SHA for 3ea6703

• shorten proof of isnormal_subgroup_commutator

  Show description for 5f19025
  Alizter

  committed
  5f19025

  Copy full SHA for 5f19025

• Subgroup: slightly simplify a couple of arguments

  

  jdchristensen

  authored and

  Alizter

  committed
  286eced

  Copy full SHA for 286eced

• Subgroup, Commutator: add and use subgroup_eq_subgroup_generated_op

  

  jdchristensen

  authored and

  Alizter

  committed
  f0c34ed

  Copy full SHA for f0c34ed