Code

image of a subgroup#2201

Code

Merged

Alizter merged 14 commits intoHoTT:masterHoTT/Coq-HoTT:masterfrom Alizter:ps/rr/image_of_a_subgroupAlizter/HoTT:ps/rr/image_of_a_subgroupCopy head branch name to clipboardJan 22, 2025

+319-240

Commits

Commits on Jan 22, 2025

• image of a subgroup

  Show description for 9e50a90
  Alizter

  committed
  9e50a90

  Copy full SHA for 9e50a90

• Subgroup: use conn_map_factor1_image and fix comment

  

  jdchristensen

  authored and

  Alizter

  committed
  f6f20fe

  Copy full SHA for f6f20fe

• export conn_map_factor1_image in Subgroup.v

  Show description for 70d25d9
  Alizter

  committed
  70d25d9

  Copy full SHA for 70d25d9

• make subgroup_group in grp_homo_subgroup_image more explicit

  Show description for 2f495e1
  Alizter

  committed
  2f495e1

  Copy full SHA for 2f495e1

• absorb Image.v into Subgroup.v

  Show description for 733b48a
  Alizter

  committed
  733b48a

  Copy full SHA for 733b48a

• rename grp_homo_subgroup_image_in

  Show description for acdcfd5
  Alizter

  committed
  acdcfd5

  Copy full SHA for acdcfd5

• absorb Kernel.v into Subgroup.v and reuse preimage for kernel

  Show description for e2f36c2
  Alizter

  committed
  e2f36c2

  Copy full SHA for e2f36c2

• move preimage to own section and fix some section headers

  Show description for bf5646d
  Alizter

  committed
  bf5646d

  Copy full SHA for bf5646d

• more comments and reorganization

  Show description for 6bb531f
  Alizter

  committed
  6bb531f

  Copy full SHA for 6bb531f

• Subgroup: add and use subgroup_corec

  

  jdchristensen

  authored and

  Alizter

  committed
  7a6440b

  Copy full SHA for 7a6440b

• Subgroup: move grp_homo_restr earlier and use it

  

  jdchristensen

  authored and

  Alizter

  committed
  5d0823f

  Copy full SHA for 5d0823f

• Subgroup: fix comments

  

  jdchristensen

  authored and

  Alizter

  committed
  5db2ab0

  Copy full SHA for 5db2ab0

• generalise equiv_grp_kernel_corec

  Show description for c8258ce
  Alizter

  committed
  c8258ce

  Copy full SHA for c8258ce

• flip direction of equiv_grp_kernel_corec

  Show description for 9f85dd5
  Alizter

  committed
  9f85dd5

  Copy full SHA for 9f85dd5