Documentation Verification Report

Option

📁 Source: Mathlib/GroupTheory/Perm/Option.lean

Statistics

Metric	Count
Definitions `decomposeOption`	1
Theorems `decomposeOption_apply`, `decomposeOption_symm_apply`, `decomposeOption_symm_of_none_apply`, `decomposeOption_symm_sign`, `optionCongr_one`, `optionCongr_sign`, `optionCongr_swap`, `univ_perm_option`, `map_equiv_removeNone`	9
Total	10

Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`optionCongr_one` 📖	mathematical	—	`optionCongr` `Perm` `Perm.instOne` `Equiv`	—	`optionCongr_refl`
`optionCongr_sign` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Perm` `Units` `Int.instMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Perm.permGroup` `Units.instMulOneClass` `MonoidHom.instFunLike` `Perm.sign` `instFintypeOption` `optionCongr`	—	`Perm.swap_induction_on` `Finite.of_fintype` `optionCongr_refl` `Perm.sign_refl` `optionCongr_trans` `optionCongr_swap` `Perm.sign_trans` `Perm.sign_swap'` `neg_mul` `one_mul`
`optionCongr_swap` 📖	mathematical	—	`optionCongr` `swap`	—	`Perm.ext` `swap_apply_of_ne_of_ne` `swap_apply_left` `swap_apply_right`

Equiv.Perm

Definitions

Name	Category	Theorems
`decomposeOption` 📖	CompOp	5 math math: `Finset.univ_perm_option`, `decomposeOption_symm_of_none_apply`, `decomposeOption_symm_sign`, `decomposeOption_symm_apply`, `decomposeOption_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`decomposeOption_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `decomposeOption` `Equiv.removeNone`	—	—
`decomposeOption_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `decomposeOption` `instMul` `Equiv.swap` `Equiv.optionCongr`	—	—
`decomposeOption_symm_of_none_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv` `Equiv.symm` `decomposeOption`	—	`Equiv.swap_self`
`decomposeOption_symm_sign` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Equiv.Perm` `Units` `Int.instMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `permGroup` `Units.instMulOneClass` `MonoidHom.instFunLike` `sign` `instFintypeOption` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `decomposeOption`	—	`Equiv.swap_self` `Equiv.optionCongr_sign`

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`univ_perm_option` 📖	mathematical	—	`univ` `Equiv.Perm` `Equiv.instFintype` `instFintypeOption` `map` `Equiv.toEmbedding` `Equiv.symm` `Equiv.Perm.decomposeOption` `instFintypeProd`	—	`univ_map_equiv_to_embedding`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_equiv_removeNone` 📖	mathematical	—	`Equiv.optionCongr` `Equiv.removeNone` `Equiv.Perm` `Equiv.Perm.instMul` `Equiv.swap` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`Equiv.Perm.ext` `Equiv.swap_apply_right` `Equiv.removeNone_none` `Equiv.swap_apply_left` `Equiv.injective` `Equiv.removeNone_some` `Equiv.swap_apply_of_ne_of_ne`

---

← Back to Index