Conj

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

Statistics

Metric	Count
Definitions `AddConjClasses`, `carrier`, `instDecidableEqOfDecidableRelIsAddConj`, `instInhabited`, `instZero`, `map`, `mk`, `mkEquiv`, `ConjClasses`, `carrier`, `instDecidableEqOfDecidableRelIsConj`, `instInhabited`, `instOne`, `map`, `mk`, `mkEquiv`, `IsAddConj`, `setoid`, `IsConj`, `setoid`, `«slow-failing_instance_priority»`, `addConjugatesOf`, `conjugatesOf`	23
Theorems `carrier_eq_preimage_mk`, `exists_rep`, `forall_isAddConj`, `map_surjective`, `mem_carrier_iff_mk_eq`, `mem_carrier_mk`, `mk_bijective`, `mk_eq_mk_iff_isAddConj`, `mk_injective`, `mk_surjective`, `quot_mk_eq_mk`, `quotient_mk_eq_mk`, `zero_eq_mk_zero`, `map_isAddConj`, `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`, `addConjugatesOf_eq`, `nsmul`, `refl`, `trans`, `conjugatesOf_eq`, `pow`, `refl`, `trans`, `map_isConj`, `addConj_add`, `addConj_injective`, `addConj_neg`, `addConj_nsmul`, `addConj_zsmul`, `conj_injective`, `conj_inv`, `conj_mul`, `conj_pow`, `conj_zpow`, `isAddConj_comm`, `isAddConj_iff`, `isAddConj_iff_addConjugatesOf_eq`, `isAddConj_iff_eq`, `isAddConj_zero_left`, `isAddConj_zero_right`, `isConj_comm`, `isConj_iff`, `isConj_iff_conjugatesOf_eq`, `isConj_iff_eq`, `isConj_one_left`, `isConj_one_right`, `mem_addConjugatesOf_self`, `mem_conjugatesOf_self`	60
Total	83

AddConjClasses

Definitions

Name	Category	Theorems
`carrier` 📖	CompOp	3 math math: `mem_carrier_iff_mk_eq`, `mem_carrier_mk`, `carrier_eq_preimage_mk`
`instDecidableEqOfDecidableRelIsAddConj` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instZero` 📖	CompOp	1 math math: `zero_eq_mk_zero`
`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` `AddConjClasses` `Set` `Set.instSingletonSet`	—	`Set.ext` `mem_carrier_iff_mk_eq`
`exists_rep` 📖	—	—	—	—	—
`forall_isAddConj` 📖	—	—	—	—	—
`map_surjective` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike`	`AddConjClasses` `map`	—	`mk_surjective`
`mem_carrier_iff_mk_eq` 📖	mathematical	—	`Set` `Set.instMembership` `carrier`	—	`forall_isAddConj` `IsAddConj.addConjugatesOf_eq` `carrier.eq_1` `mk_eq_mk_iff_isAddConj`
`mem_carrier_mk` 📖	mathematical	—	`Set` `Set.instMembership` `carrier`	—	`IsAddConj.refl`
`mk_bijective` 📖	mathematical	—	`Function.Bijective` `AddConjClasses` `AddCommMonoid.toAddMonoid`	—	`mk_injective` `mk_surjective`
`mk_eq_mk_iff_isAddConj` 📖	mathematical	—	`IsAddConj`	—	—
`mk_injective` 📖	mathematical	—	`AddConjClasses` `AddCommMonoid.toAddMonoid`	—	`mk_eq_mk_iff_isAddConj` `isAddConj_iff_eq`
`mk_surjective` 📖	mathematical	—	`AddConjClasses`	—	`forall_isAddConj`
`quot_mk_eq_mk` 📖	mathematical	—	`IsAddConj.setoid`	—	—
`quotient_mk_eq_mk` 📖	mathematical	—	`IsAddConj.setoid`	—	—
`zero_eq_mk_zero` 📖	mathematical	—	`AddConjClasses` `instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	—

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_isAddConj` 📖	mathematical	`IsAddConj`	`IsAddConj` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instFunLike`	—	`AddUnits.coe_map` `AddSemiconjBy.eq_1` `map_add` `AddSemiconjBy.eq`

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`	—	—

IsAddConj

Definitions

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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addConjugatesOf_eq` 📖	mathematical	`IsAddConj`	`addConjugatesOf`	—	`Set.ext` `trans` `symm`
`nsmul` 📖	mathematical	`IsAddConj`	`IsAddConj` `AddMonoid.toNSMul`	—	`AddSemiconjBy.nsmul_right`
`refl` 📖	mathematical	—	`IsAddConj`	—	`AddSemiconjBy.zero_left`
`trans` 📖	mathematical	`IsAddConj`	`IsAddConj`	—	`AddSemiconjBy.add_left`

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`	`IsConj` `Monoid.toPow`	—	`SemiconjBy.pow_right`
`refl` 📖	mathematical	—	`IsConj`	—	`SemiconjBy.one_left`
`trans` 📖	mathematical	`IsConj`	`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`	`IsConj` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instFunLike`	—	`Units.coe_map` `SemiconjBy.eq_1` `map_mul` `SemiconjBy.eq`

(root)

Definitions

Name	Category	Theorems
`AddConjClasses` 📖	CompOp	6 math math: `AddConjClasses.mk_surjective`, `AddConjClasses.mk_injective`, `AddConjClasses.map_surjective`, `AddConjClasses.mk_bijective`, `AddConjClasses.carrier_eq_preimage_mk`, `AddConjClasses.zero_eq_mk_zero`
`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`
`IsAddConj` 📖	MathDef	13 math math: `IsAddConj.nsmul`, `AddMonoidHom.map_isAddConj`, `isAddConj_iff_addConjugatesOf_eq`, `AddConjClasses.mk_eq_mk_iff_isAddConj`, `AddGroup.mem_addConjugatesOfSet_iff`, `isAddConj_iff`, `IsAddConj.symm`, `isAddConj_zero_right`, `isAddConj_comm`, `isAddConj_zero_left`, `isAddConj_iff_eq`, `IsAddConj.trans`, `IsAddConj.refl`
`IsConj` 📖	MathDef	31 math math: `isConj_one_left`, `isConj_iff`, `IsConj.symm`, `IsArithFrobAt.exists_primesOver_isConj`, `GroupWithZero.isConj_iff₀`, `Equiv.Perm.isConj_of_cycleType_eq`, `isConj_iff_conjugatesOf_eq`, `IsConj.trans`, `Equiv.Perm.card_isConj_eq`, `Equiv.Perm.isConj_swap`, `alternatingGroup.isConj_of`, `isConj_one_right`, `ConjClasses.mk_eq_mk_iff_isConj`, `isConj_iff_eq`, `Group.mem_conjugatesOfSet_iff`, `Equiv.Perm.isConj_of_support_equiv`, `IsConj.refl`, `IsConj.pow`, `Equiv.Perm.isConj_iff_cycleType_eq`, `ConjAct.mem_orbit_conjAct`, `MonoidHom.map_isConj`, `alternatingGroup.isConj_swap_mul_swap_of_cycleType_two`, `ConjAct.orbitRel_conjAct`, `Equiv.Perm.Disjoint.isConj_mul`, `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`
`addConjugatesOf` 📖	CompOp	4 math math: `AddGroup.addConjugates_subset_normal`, `IsAddConj.addConjugatesOf_eq`, `isAddConj_iff_addConjugatesOf_eq`, `mem_addConjugatesOf_self`
`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
`addConj_add` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`add_assoc` `neg_add_cancel_left`
`addConj_injective` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`addConj_neg` 📖	mathematical	—	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`add_assoc` `neg_add_rev` `neg_neg`
`addConj_nsmul` 📖	mathematical	—	`AddMonoid.toNSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`zero_nsmul` `add_zero` `add_neg_cancel` `succ_nsmul` `addConj_add`
`addConj_zsmul` 📖	mathematical	—	`SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`natCast_zsmul` `addConj_nsmul` `negSucc_zsmul` `neg_add_rev` `neg_neg` `add_assoc`
`conj_injective` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`RightCancelSemigroup.toIsRightCancelMul` `LeftCancelSemigroup.toIsLeftCancelMul`
`conj_inv` 📖	mathematical	—	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`mul_assoc` `mul_inv_rev` `inv_inv`
`conj_mul` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`mul_assoc` `inv_mul_cancel_left`
`conj_pow` 📖	mathematical	—	`Monoid.toPow` `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`
`isAddConj_comm` 📖	mathematical	—	`IsAddConj`	—	`IsAddConj.symm`
`isAddConj_iff` 📖	mathematical	—	`IsAddConj` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`add_neg_eq_iff_eq_add` `add_neg_cancel` `neg_add_cancel`
`isAddConj_iff_addConjugatesOf_eq` 📖	mathematical	—	`IsAddConj` `addConjugatesOf`	—	`IsAddConj.addConjugatesOf_eq` `mem_addConjugatesOf_self`
`isAddConj_iff_eq` 📖	mathematical	—	`IsAddConj` `AddCommMonoid.toAddMonoid`	—	`add_zero` `AddUnits.add_neg` `add_assoc` `AddUnits.add_neg_eq_iff_eq_add` `add_comm` `AddSemiconjBy.eq_1` `IsAddConj.refl`
`isAddConj_zero_left` 📖	mathematical	—	`IsAddConj` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`IsAddConj.symm` `isAddConj_zero_right`
`isAddConj_zero_right` 📖	mathematical	—	`IsAddConj` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`IsAddUnit.add_eq_right` `AddUnits.isAddUnit` `add_zero` `AddSemiconjBy.eq_1` `IsAddConj.refl`
`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_addConjugatesOf_self` 📖	mathematical	—	`Set` `Set.instMembership` `addConjugatesOf`	—	`IsAddConj.refl`
`mem_conjugatesOf_self` 📖	mathematical	—	`Set` `Set.instMembership` `conjugatesOf`	—	`IsConj.refl`

---

← Back to Index