Documentation Verification Report

RegularWreathProduct

📁 Source: Mathlib/GroupTheory/RegularWreathProduct.lean

Statistics

Metric	Count
Definitions `IteratedWreathProduct`, `RegularWreathProduct`, `equivProd`, `inl`, `instGroup`, `instInhabited`, `instInv`, `instMul`, `instMulActionProd`, `instOne`, `instSMulProd`, `left`, `right`, `rightHom`, `toPerm`, `mulEquivIteratedWreathProduct`, `instGroupIteratedWreathProduct`, `iteratedWreathToPermHom`, `«term_≀ᵣ_»`	19
Theorems `card`, `IteratedWreathProduct_succ`, `IteratedWreathProduct_zero`, `card`, `ext`, `ext_iff`, `fun_id`, `instFaithfulSMulProdOfNonempty`, `instFinite`, `inv_left`, `inv_right`, `left_inl`, `mul_def`, `mul_left`, `mul_right`, `one_left`, `one_right`, `rightHom_comp_inl_eq_id`, `rightHom_eq_right`, `right_inl`, `smul_def`, `toPermInj`, `instFiniteIteratedWreathProduct`, `iteratedWreathToPermHomInj`	24
Total	43

IteratedWreathProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card` 📖	mathematical	—	`Nat.card` `IteratedWreathProduct` `Monoid.toNatPow` `Nat.instMonoid` `Finset.sum` `Nat.instAddCommMonoid` `Finset.range`	—	`Nat.card_eq_fintype_card` `Fintype.card_unique` `pow_zero` `IteratedWreathProduct_succ` `RegularWreathProduct.card` `geom_sum_succ` `pow_succ` `pow_mul'`

RegularWreathProduct

Definitions

Name	Category	Theorems
`equivProd` 📖	CompOp	—
`inl` 📖	CompOp	4 math math: `left_inl`, `fun_id`, `right_inl`, `rightHom_comp_inl_eq_id`
`instGroup` 📖	CompOp	6 math math: `left_inl`, `toPermInj`, `fun_id`, `right_inl`, `rightHom_eq_right`, `rightHom_comp_inl_eq_id`
`instInhabited` 📖	CompOp	—
`instInv` 📖	CompOp	2 math math: `inv_left`, `inv_right`
`instMul` 📖	CompOp	3 math math: `mul_right`, `mul_def`, `mul_left`
`instMulActionProd` 📖	CompOp	—
`instOne` 📖	CompOp	2 math math: `one_right`, `one_left`
`instSMulProd` 📖	CompOp	2 math math: `smul_def`, `instFaithfulSMulProdOfNonempty`
`left` 📖	CompOp	7 math math: `ext_iff`, `smul_def`, `left_inl`, `inv_left`, `one_left`, `mul_def`, `mul_left`
`right` 📖	CompOp	10 math math: `ext_iff`, `smul_def`, `inv_left`, `right_inl`, `one_right`, `rightHom_eq_right`, `inv_right`, `mul_right`, `mul_def`, `mul_left`
`rightHom` 📖	CompOp	3 math math: `fun_id`, `rightHom_eq_right`, `rightHom_comp_inl_eq_id`
`toPerm` 📖	CompOp	1 math math: `toPermInj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card` 📖	mathematical	—	`Nat.card` `RegularWreathProduct` `Monoid.toNatPow` `Nat.instMonoid`	—	`Nat.card_congr` `Nat.card_prod` `Nat.card_fun`
`ext` 📖	—	`left` `right`	—	—	—
`ext_iff` 📖	mathematical	—	`left` `right`	—	`ext`
`fun_id` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `RegularWreathProduct` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `MonoidHom.instFunLike` `rightHom` `inl`	—	—
`instFaithfulSMulProdOfNonempty` 📖	mathematical	—	`FaithfulSMul` `RegularWreathProduct` `instSMulProd`	—	`RightCancelSemigroup.toIsRightCancelMul` `ext` `FaithfulSMul.eq_of_smul_eq_smul` `add_neg_cancel` `zpow_zero` `one_mul`
`instFinite` 📖	mathematical	—	`Finite` `RegularWreathProduct`	—	`Finite.of_equiv` `Finite.instProd` `Pi.finite`
`inv_left` 📖	mathematical	—	`left` `RegularWreathProduct` `instInv` `Pi.instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `right`	—	—
`inv_right` 📖	mathematical	—	`right` `RegularWreathProduct` `instInv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`left_inl` 📖	mathematical	—	`left` `DFunLike.coe` `MonoidHom` `RegularWreathProduct` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `MonoidHom.instFunLike` `inl` `Pi.instOne` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`mul_def` 📖	mathematical	—	`RegularWreathProduct` `instMul` `Pi.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `left` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `right`	—	—
`mul_left` 📖	mathematical	—	`left` `RegularWreathProduct` `instMul` `Pi.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `right`	—	—
`mul_right` 📖	mathematical	—	`right` `RegularWreathProduct` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`one_left` 📖	mathematical	—	`left` `RegularWreathProduct` `instOne` `Pi.instOne` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`one_right` 📖	mathematical	—	`right` `RegularWreathProduct` `instOne` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	—
`rightHom_comp_inl_eq_id` 📖	mathematical	—	`MonoidHom.comp` `RegularWreathProduct` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `rightHom` `inl` `MonoidHom.id`	—	`MonoidHom.ext`
`rightHom_eq_right` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `RegularWreathProduct` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `MonoidHom.instFunLike` `rightHom` `right`	—	—
`right_inl` 📖	mathematical	—	`right` `DFunLike.coe` `MonoidHom` `RegularWreathProduct` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `MonoidHom.instFunLike` `inl`	—	—
`smul_def` 📖	mathematical	—	`RegularWreathProduct` `instSMulProd` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `left` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `right`	—	—
`toPermInj` 📖	mathematical	—	`RegularWreathProduct` `Equiv.Perm` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `Equiv.Perm.permGroup` `MonoidHom.instFunLike` `toPerm`	—	`MulAction.toPerm_injective` `instFaithfulSMulProdOfNonempty` `One.instNonempty`

Sylow

Definitions

Name	Category	Theorems
`mulEquivIteratedWreathProduct` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`IteratedWreathProduct` 📖	CompOp	5 math math: `IteratedWreathProduct.card`, `instFiniteIteratedWreathProduct`, `iteratedWreathToPermHomInj`, `IteratedWreathProduct_succ`, `IteratedWreathProduct_zero`
`RegularWreathProduct` 📖	CompData	18 math math: `RegularWreathProduct.card`, `RegularWreathProduct.smul_def`, `RegularWreathProduct.instFinite`, `RegularWreathProduct.left_inl`, `RegularWreathProduct.toPermInj`, `RegularWreathProduct.fun_id`, `RegularWreathProduct.inv_left`, `RegularWreathProduct.right_inl`, `RegularWreathProduct.one_right`, `RegularWreathProduct.rightHom_eq_right`, `RegularWreathProduct.rightHom_comp_inl_eq_id`, `RegularWreathProduct.one_left`, `RegularWreathProduct.inv_right`, `RegularWreathProduct.mul_right`, `RegularWreathProduct.mul_def`, `IteratedWreathProduct_succ`, `RegularWreathProduct.mul_left`, `RegularWreathProduct.instFaithfulSMulProdOfNonempty`
`instGroupIteratedWreathProduct` 📖	CompOp	1 math math: `iteratedWreathToPermHomInj`
`iteratedWreathToPermHom` 📖	CompOp	1 math math: `iteratedWreathToPermHomInj`
`«term_≀ᵣ_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`IteratedWreathProduct_succ` 📖	mathematical	—	`IteratedWreathProduct` `RegularWreathProduct`	—	—
`IteratedWreathProduct_zero` 📖	mathematical	—	`IteratedWreathProduct`	—	—
`instFiniteIteratedWreathProduct` 📖	mathematical	—	`Finite` `IteratedWreathProduct`	—	`IteratedWreathProduct_zero` `Finite.of_fintype` `IteratedWreathProduct_succ` `RegularWreathProduct.instFinite`
`iteratedWreathToPermHomInj` 📖	mathematical	—	`IteratedWreathProduct` `Equiv.Perm` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroupIteratedWreathProduct` `Equiv.Perm.permGroup` `MonoidHom.instFunLike` `iteratedWreathToPermHom`	—	`Function.injective_of_subsingleton` `Equiv.ext` `Equiv.comp_injective` `RegularWreathProduct.toPermInj` `One.instNonempty`

---

← Back to Index