Documentation Verification Report

Conj

📁 Source: Mathlib/Algebra/Group/Conj.lean

Statistics

Metric	Count
Definitions `ConjClasses`, `carrier`, `instDecidableEqOfDecidableRelIsConj`, `instInhabited`, `instOne`, `map`, `mk`, `mkEquiv`, `IsConj`, `setoid`, `«slow-failing_instance_priority»`, `conjugatesOf`	12
Theorems `carrier_eq_preimage_mk`, `exists_rep`, `forall_isConj`, `map_surjective`, `mem_carrier_iff_mk_eq`, `mem_carrier_mk`, `mk_bijective`, `mk_eq_mk_iff_isConj`, `mk_injective`, `mk_surjective`, `one_eq_mk_one`, `quot_mk_eq_mk`, `quotient_mk_eq_mk`, `conjugatesOf_eq`, `pow`, `refl`, `trans`, `map_isConj`, `conj_injective`, `conj_inv`, `conj_mul`, `conj_pow`, `conj_zpow`, `isConj_comm`, `isConj_iff`, `isConj_iff_conjugatesOf_eq`, `isConj_iff_eq`, `isConj_one_left`, `isConj_one_right`, `mem_conjugatesOf_self`	30
Total	42

ConjClasses

Definitions

Name	Category	Theorems
`carrier` 📖	CompOp	10 math math: `carrier_eq_preimage_mk`, `mem_carrier_iff_mk_eq`, `sum_conjClasses_card_eq_card`, `mem_noncenter`, `ConjAct.orbit_eq_carrier_conjClasses`, `Group.nat_card_center_add_sum_card_noncenter_eq_card`, `Group.card_center_add_sum_card_noncenter_eq_card`, `card_carrier`, `mem_carrier_mk`, `Group.sum_card_conj_classes_eq_card`
`instDecidableEqOfDecidableRelIsConj` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instOne` 📖	CompOp	1 math math: `one_eq_mk_one`
`map` 📖	CompOp	1 math math: `map_surjective`
`mk` 📖	CompOp	—
`mkEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`carrier_eq_preimage_mk` 📖	mathematical	—	`carrier` `Set.preimage` `ConjClasses` `Set` `Set.instSingletonSet`	—	`Set.ext` `mem_carrier_iff_mk_eq`
`exists_rep` 📖	—	—	—	—	—
`forall_isConj` 📖	—	—	—	—	—
`map_surjective` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike`	`ConjClasses` `map`	—	`mk_surjective`
`mem_carrier_iff_mk_eq` 📖	mathematical	—	`Set` `Set.instMembership` `carrier`	—	`forall_isConj` `IsConj.conjugatesOf_eq` `carrier.eq_1` `mk_eq_mk_iff_isConj`
`mem_carrier_mk` 📖	mathematical	—	`Set` `Set.instMembership` `carrier`	—	`IsConj.refl`
`mk_bijective` 📖	mathematical	—	`Function.Bijective` `ConjClasses` `CommMonoid.toMonoid`	—	`mk_injective` `mk_surjective`
`mk_eq_mk_iff_isConj` 📖	mathematical	—	`IsConj`	—	—
`mk_injective` 📖	mathematical	—	`ConjClasses` `CommMonoid.toMonoid`	—	`mk_eq_mk_iff_isConj` `isConj_iff_eq`
`mk_surjective` 📖	mathematical	—	`ConjClasses`	—	`forall_isConj`
`one_eq_mk_one` 📖	mathematical	—	`ConjClasses` `instOne` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—
`quot_mk_eq_mk` 📖	mathematical	—	`IsConj.setoid`	—	—
`quotient_mk_eq_mk` 📖	mathematical	—	`IsConj.setoid`	—	—

IsConj

Definitions

Name	Category	Theorems
`setoid` 📖	CompOp	2 math math: `ConjClasses.quotient_mk_eq_mk`, `ConjClasses.quot_mk_eq_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conjugatesOf_eq` 📖	mathematical	`IsConj`	`conjugatesOf`	—	`Set.ext` `trans` `symm`
`pow` 📖	mathematical	`IsConj`	`Monoid.toNatPow`	—	`SemiconjBy.pow_right`
`refl` 📖	mathematical	—	`IsConj`	—	`SemiconjBy.one_left`
`trans` 📖	—	`IsConj`	—	—	`SemiconjBy.mul_left`

LibraryNote

Definitions

Name	Category	Theorems
`«slow-failing_instance_priority»` 📖	CompOp	—

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_isConj` 📖	mathematical	`IsConj`	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instFunLike`	—	`Units.coe_map` `SemiconjBy.eq_1` `map_mul` `SemiconjBy.eq`

(root)

Definitions

Name	Category	Theorems
`ConjClasses` 📖	CompOp	16 math math: `ConjClasses.carrier_eq_preimage_mk`, `ConjClasses.one_eq_mk_one`, `card_comm_eq_card_conjClasses_mul_card`, `ConjClasses.mk_injective`, `sum_conjClasses_card_eq_card`, `ConjClasses.mem_noncenter`, `ConjClasses.mk_bijOn`, `ConjClasses.mk_surjective`, `DihedralGroup.card_conjClasses_odd`, `ConjClasses.mk_bijective`, `commProb_def'`, `Group.nat_card_center_add_sum_card_noncenter_eq_card`, `instFiniteConjClasses`, `Group.card_center_add_sum_card_noncenter_eq_card`, `Group.sum_card_conj_classes_eq_card`, `ConjClasses.map_surjective`
`IsConj` 📖	MathDef	25 math math: `isConj_one_left`, `isConj_iff`, `IsArithFrobAt.exists_primesOver_isConj`, `GroupWithZero.isConj_iff₀`, `Equiv.Perm.isConj_of_cycleType_eq`, `isConj_iff_conjugatesOf_eq`, `Equiv.Perm.card_isConj_eq`, `Equiv.Perm.isConj_swap`, `isConj_one_right`, `ConjClasses.mk_eq_mk_iff_isConj`, `isConj_iff_eq`, `Group.mem_conjugatesOfSet_iff`, `Equiv.Perm.isConj_of_support_equiv`, `IsConj.refl`, `Equiv.Perm.isConj_iff_cycleType_eq`, `ConjAct.mem_orbit_conjAct`, `alternatingGroup.isConj_swap_mul_swap_of_cycleType_two`, `ConjAct.orbitRel_conjAct`, `Equiv.Perm.partition_eq_of_isConj`, `alternatingGroup.isThreeCycle_isConj`, `Equiv.Perm.card_isConj_mul_eq`, `isConj_comm`, `Equiv.Perm.IsCycle.isConj_iff`, `Equiv.Perm.IsCycle.isConj`, `isConj_arithFrobAt`
`conjugatesOf` 📖	CompOp	4 math math: `Group.conjugates_subset_normal`, `isConj_iff_conjugatesOf_eq`, `mem_conjugatesOf_self`, `IsConj.conjugatesOf_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conj_injective` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`MulEquiv.injective`
`conj_inv` 📖	mathematical	—	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`map_inv` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass`
`conj_mul` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`map_mul` `MonoidHomClass.toMulHomClass` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass`
`conj_pow` 📖	mathematical	—	`Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`pow_zero` `mul_one` `mul_inv_cancel` `pow_succ` `conj_mul`
`conj_zpow` 📖	mathematical	—	`DivInvMonoid.toZPow` `Group.toDivInvMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`zpow_natCast` `conj_pow` `zpow_negSucc` `mul_inv_rev` `inv_inv` `mul_assoc`
`isConj_comm` 📖	mathematical	—	`IsConj`	—	`IsConj.symm`
`isConj_iff` 📖	mathematical	—	`IsConj` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`mul_inv_eq_iff_eq_mul` `mul_inv_cancel` `inv_mul_cancel`
`isConj_iff_conjugatesOf_eq` 📖	mathematical	—	`IsConj` `conjugatesOf`	—	`IsConj.conjugatesOf_eq` `mem_conjugatesOf_self`
`isConj_iff_eq` 📖	mathematical	—	`IsConj` `CommMonoid.toMonoid`	—	`mul_one` `Units.mul_inv` `mul_assoc` `Units.mul_inv_eq_iff_eq_mul` `mul_comm` `SemiconjBy.eq_1` `IsConj.refl`
`isConj_one_left` 📖	mathematical	—	`IsConj` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`IsConj.symm` `isConj_one_right`
`isConj_one_right` 📖	mathematical	—	`IsConj` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`IsUnit.mul_eq_right` `Units.isUnit` `mul_one` `SemiconjBy.eq_1` `IsConj.refl`
`mem_conjugatesOf_self` 📖	mathematical	—	`Set` `Set.instMembership` `conjugatesOf`	—	`IsConj.refl`

---

← Back to Index