Documentation Verification Report

DomMulAct

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

Statistics

Metric	Count
Definitions `stabilizerEquiv_invFun`, `stabilizerEquiv_invFun_aux`, `stabilizerMulEquiv`	3
Theorems `comp_stabilizerEquiv_invFun`, `mem_stabilizer_iff`, `stabilizerEquiv_invFun_eq`, `stabilizerMulEquiv_apply`, `stabilizer_card`, `stabilizer_card'`, `stabilizer_ncard`	7
Total	10

DomMulAct

Definitions

Name	Category	Theorems
`stabilizerEquiv_invFun` 📖	CompOp	2 math math: `comp_stabilizerEquiv_invFun`, `stabilizerEquiv_invFun_eq`
`stabilizerEquiv_invFun_aux` 📖	CompOp	—
`stabilizerMulEquiv` 📖	CompOp	1 math math: `stabilizerMulEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_stabilizerEquiv_invFun` 📖	mathematical	—	`stabilizerEquiv_invFun`	—	`Subtype.prop`
`mem_stabilizer_iff` 📖	mathematical	—	`DomMulAct` `Equiv.Perm` `Subgroup` `instGroupOfMulOpposite` `MulOpposite.instGroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulAction.stabilizer` `instMulActionForall` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.applyMulAction` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv` `Equiv.symm`	—	—
`stabilizerEquiv_invFun_eq` 📖	mathematical	—	`stabilizerEquiv_invFun` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	—
`stabilizerMulEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `MulEquiv` `MulOpposite` `DomMulAct` `Subgroup` `instGroupOfMulOpposite` `MulOpposite.instGroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulAction.stabilizer` `instMulActionForall` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Equiv.Perm.applyMulAction` `MulOpposite.instMul` `Subgroup.mul` `Pi.instMul` `Equiv.Perm.instMul` `MulEquiv.instEquivLike` `stabilizerMulEquiv` `Equiv` `Equiv.symm` `MulOpposite.unop`	—	—
`stabilizer_card` 📖	mathematical	—	`Fintype.card` `Equiv.Perm` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike` `Subtype.fintype` `Fintype.decidablePiFintype` `Equiv.instFintype` `Finset.prod` `Nat.instCommMonoid` `Finset.univ` `Nat.factorial`	—	`Nat.card_eq_fintype_card` `Nat.card_congr` `Nat.card_pi` `Finset.prod_congr` `Fintype.card_perm`
`stabilizer_card'` 📖	mathematical	—	`Fintype.card` `Equiv.Perm` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike` `Subtype.fintype` `Fintype.decidablePiFintype` `Equiv.instFintype` `Finset.prod` `Nat.instCommMonoid` `Finset.image` `Finset.univ` `Nat.factorial`	—	`Finset.coe_image` `Finset.coe_univ` `Set.image_univ` `Fintype.card_congr'` `stabilizer_card` `Finset.prod_bij` `Finset.coe_mem` `SetCoe.ext` `Fintype.card_congr` `Equiv.refl_apply`
`stabilizer_ncard` 📖	mathematical	—	`Set.ncard` `Equiv.Perm` `setOf` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike` `Finset.prod` `Nat.instCommMonoid` `Finset.univ` `Nat.factorial`	—	`nonempty_fintype` `Nat.card_eq_fintype_card` `Finset.prod_congr` `stabilizer_card`

---

← Back to Index