Documentation

LeanPool.Kurosh

Kurosh and Schreier subgroup theorems via covering graphs #

Source: doi:10.1007/BF01449159, url:https://github.com/Arthur742Ramos/KuroshSubgroupTheorem Authors: Arthur Freitas Ramos, David Barros Hulak, Ruy J. G. B. de Queiroz Status: verified Main declarations: GraphCoveringTheory.KuroshStatement.kurosh_decomposition_with_inclusions Tags: group-theory, free-products, bass-serre-theory, schreier-index-formula, covering-graphs MSC: 20E07, 05C25, 18B40