Kurosh Raw Path Value

Adapted for Lean Pool from Arthur742Ramos/KuroshSubgroupTheorem, commit 911707126c8b9bb0c764bf853008fe1053c0aad9: imports, API compatibility, and proof organization were revised.

@[instance_reducible]

noncomputable def GraphCoveringTheory.Kurosh.kuroshRawPathValueDecidableEq (α : Type u_1) : DecidableEq α

Classical equality used locally in this part of the Kurosh construction.

Equations

• GraphCoveringTheory.Kurosh.kuroshRawPathValueDecidableEq α = Classical.decEq α

theorem GraphCoveringTheory.Kurosh.Internal.coverPathValue_rawTree {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {a : RawBassSerreOrbitVertex G H} (p : Quiver.Path (rawBassSerreOrbitRoot G H) a) : coverPathValue G H (rawTreePathMap G H p) = 1