Documentation Verification Report

Card

📁 Source: Mathlib/GroupTheory/Coset/Card.lean

Statistics

Metric	Count
Definitions `fintype`, `fintypeQuotientRightRel`, `fintype`, `fintypeQuotientRightRel`	4
Theorems `card_addSubgroup_dvd_card`, `card_add_eq_card_addSubgroup_add_card_quotient`, `card_comap_dvd_of_injective`, `card_dvd_of_injective`, `card_dvd_of_le`, `card_eq_card_quotient_mul_card_addSubgroup`, `card_quotient_dvd_card`, `card_quotient_rightRel`, `finite`, `card_quotient_rightRel`, `finite`, `card_comap_dvd_of_injective`, `card_dvd_of_injective`, `card_dvd_of_le`, `card_eq_card_quotient_mul_card_subgroup`, `card_mul_eq_card_subgroup_mul_card_quotient`, `card_quotient_dvd_card`, `card_subgroup_dvd_card`	18
Total	22

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_addSubgroup_dvd_card` 📖	mathematical	—	`Nat.card` `AddSubgroup` `SetLike.instMembership` `instSetLike`	—	`card_eq_card_quotient_mul_card_addSubgroup` `dvd_mul_left`
`card_add_eq_card_addSubgroup_add_card_quotient` 📖	mathematical	—	`Nat.card` `Set.Elem` `Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SetLike.coe` `AddSubgroup` `instSetLike` `SetLike.instMembership` `HasQuotient.Quotient` `QuotientAddGroup.instHasQuotientAddSubgroup` `Set.image`	—	`Nat.card_prod` `Nat.card_congr` `Set.ext` `Set.mem_iUnion` `Set.mem_preimage` `Set.mem_add` `SetLike.mem_coe` `NegMemClass.neg_mem` `AddSubgroupClass.toNegMemClass` `instAddSubgroupClass` `add_neg_cancel_right`
`card_comap_dvd_of_injective` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike`	`Nat.card` `AddSubgroup` `SetLike.instMembership` `instSetLike` `comap`	—	`Nat.card_congr` `card_dvd_of_le` `map_comap_le`
`card_dvd_of_injective` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddMonoidHom.instFunLike`	`Nat.card`	—	`Nat.card_congr` `card_addSubgroup_dvd_card`
`card_dvd_of_le` 📖	mathematical	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Nat.card` `SetLike.instMembership` `instSetLike`	—	`card_dvd_of_injective` `inclusion_injective`
`card_eq_card_quotient_mul_card_addSubgroup` 📖	mathematical	—	`Nat.card` `HasQuotient.Quotient` `AddSubgroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `SetLike.instMembership` `instSetLike`	—	`Nat.card_prod` `Nat.card_congr`
`card_quotient_dvd_card` 📖	mathematical	—	`Nat.card` `HasQuotient.Quotient` `AddSubgroup` `QuotientAddGroup.instHasQuotientAddSubgroup`	—	`card_eq_card_quotient_mul_card_addSubgroup` `dvd_mul_right`

QuotientAddGroup

Definitions

Name	Category	Theorems
`fintype` 📖	CompOp	—
`fintypeQuotientRightRel` 📖	CompOp	1 math math: `card_quotient_rightRel`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_quotient_rightRel` 📖	mathematical	—	`Fintype.card` `rightRel` `fintypeQuotientRightRel` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup`	—	`Fintype.ofEquiv_card`
`finite` 📖	mathematical	—	`Finite` `HasQuotient.Quotient` `AddSubgroup` `instHasQuotientAddSubgroup`	—	`Quotient.finite`

QuotientGroup

Definitions

Name	Category	Theorems
`fintype` 📖	CompOp	2 math math: `AlternatingMap.domCoprod_coe`, `AlternatingMap.domCoprod_apply`
`fintypeQuotientRightRel` 📖	CompOp	2 math math: `card_quotient_rightRel`, `Rep.coindToInd_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_quotient_rightRel` 📖	mathematical	—	`Fintype.card` `rightRel` `fintypeQuotientRightRel` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup`	—	`Fintype.ofEquiv_card`
`finite` 📖	mathematical	—	`Finite` `HasQuotient.Quotient` `Subgroup` `instHasQuotientSubgroup`	—	`Quotient.finite`

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_comap_dvd_of_injective` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	`Nat.card` `Subgroup` `SetLike.instMembership` `instSetLike` `comap`	—	`Nat.card_congr` `card_dvd_of_le` `map_comap_le`
`card_dvd_of_injective` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	`Nat.card`	—	`Nat.card_congr` `card_subgroup_dvd_card`
`card_dvd_of_le` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Nat.card` `SetLike.instMembership` `instSetLike`	—	`card_dvd_of_injective` `inclusion_injective`
`card_eq_card_quotient_mul_card_subgroup` 📖	mathematical	—	`Nat.card` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `SetLike.instMembership` `instSetLike`	—	`Nat.card_prod` `Nat.card_congr`
`card_mul_eq_card_subgroup_mul_card_quotient` 📖	mathematical	—	`Nat.card` `Set.Elem` `Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.coe` `Subgroup` `instSetLike` `SetLike.instMembership` `HasQuotient.Quotient` `QuotientGroup.instHasQuotientSubgroup` `Set.image`	—	`Nat.card_prod` `Nat.card_congr` `Set.ext` `InvMemClass.inv_mem` `SubgroupClass.toInvMemClass` `instSubgroupClass` `mul_inv_cancel_right`
`card_quotient_dvd_card` 📖	mathematical	—	`Nat.card` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup`	—	`card_eq_card_quotient_mul_card_subgroup` `dvd_mul_right`
`card_subgroup_dvd_card` 📖	mathematical	—	`Nat.card` `Subgroup` `SetLike.instMembership` `instSetLike`	—	`card_eq_card_quotient_mul_card_subgroup` `dvd_mul_left`

---

← Back to Index