Documentation Verification Report

FundamentalGroup

📁 Source: Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean

Statistics

Metric	Count
Definitions `FundamentalGroup`, `fromArrow`, `fromPath`, `fundamentalGroupMulEquivOfPath`, `fundamentalGroupMulEquivOfPathConnected`, `map`, `mapOfEq`, `toArrow`, `toPath`, `instGroupFundamentalGroup`, `instInhabitedFundamentalGroup`	11
Theorems `mapOfEq_apply`, `map_apply`	2
Total	13

FundamentalGroup

Definitions

Name	Category	Theorems
`fromArrow` 📖	CompOp	—
`fromPath` 📖	CompOp	1 math math: `mapOfEq_apply`
`fundamentalGroupMulEquivOfPath` 📖	CompOp	—
`fundamentalGroupMulEquivOfPathConnected` 📖	CompOp	—
`map` 📖	CompOp	1 math math: `map_apply`
`mapOfEq` 📖	CompOp	1 math math: `mapOfEq_apply`
`toArrow` 📖	CompOp	—
`toPath` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mapOfEq_apply` 📖	mathematical	`DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike`	`MonoidHom` `FundamentalGroup` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroupFundamentalGroup` `MonoidHom.instFunLike` `mapOfEq` `fromPath` `Path.cast` `Path.map` `ContinuousMap.continuous`	—	`FundamentalGroupoid.conj_eqToHom` `ContinuousMap.continuous`
`map_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `FundamentalGroup` `ContinuousMap` `ContinuousMap.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroupFundamentalGroup` `MonoidHom.instFunLike` `map` `Path.Homotopic.Quotient.map`	—	—

(root)

Definitions

Name	Category	Theorems
`FundamentalGroup` 📖	CompOp	2 math math: `FundamentalGroup.map_apply`, `FundamentalGroup.mapOfEq_apply`
`instGroupFundamentalGroup` 📖	CompOp	2 math math: `FundamentalGroup.map_apply`, `FundamentalGroup.mapOfEq_apply`
`instInhabitedFundamentalGroup` 📖	CompOp	—

---

← Back to Index