Centralizer

📁 Source: Mathlib/GroupTheory/Subgroup/Centralizer.lean

Statistics

Metric	Count
Definitions centralizer, closureAddCommGroupOfComm, centralizer, closureCommGroupOfComm, instMulDistribMulActionSubtypeMemNormalizer, normalizerMonoidHom	6
Theorems center_eq_iInf, center_eq_infi', center_le_centralizer, centralizer_closure, centralizer_eq_iInf, centralizer_eq_top_iff_subset, centralizer_le, centralizer_univ, characteristic_centralizer, closure_le_centralizer_centralizer, le_centralizer, le_centralizer_iff, le_centralizer_iff_isAddCommutative, map_centralizer_le_centralizer_image, mem_centralizer_iff, mem_centralizer_iff_commutator_eq_zero, mem_centralizer_singleton_iff, normal_centralizer, center_eq_iInf, center_eq_infi', center_le_centralizer, centralizer_closure, centralizer_eq_iInf, centralizer_eq_top_iff_subset, centralizer_le, centralizer_univ, characteristic_centralizer, closure_le_centralizer_centralizer, le_centralizer, le_centralizer_iff, le_centralizer_iff_isMulCommutative, map_centralizer_le_centralizer_image, mem_centralizer_iff, mem_centralizer_iff_commutator_eq_one, mem_centralizer_singleton_iff, normal_centralizer, normalizerMonoidHom_apply_apply_coe, normalizerMonoidHom_apply_symm_apply_coe, normalizerMonoidHom_ker, smul_coe	40
Total	46

AddSubgroup

Definitions

Name	Category	Theorems
centralizer 📖	CompOp	18 math math: centralizer_eq_iInf, le_centralizer_iff, closure_le_centralizer_centralizer, mem_centralizer_iff_commutator_eq_zero, characteristic_centralizer, centralizer_closure, center_eq_infi', le_centralizer_iff_isAddCommutative, centralizer_le, mem_centralizer_iff, centralizer_eq_top_iff_subset, normal_centralizer, center_eq_iInf, centralizer_univ, center_le_centralizer, le_centralizer, mem_centralizer_singleton_iff, map_centralizer_le_centralizer_image
closureAddCommGroupOfComm 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
center_eq_iInf 📖	mathematical	closure Top.top AddSubgroup instTop	center iInf instInfSet Set Set.instMembership centralizer Set.instSingletonSet	—	centralizer_univ coe_top centralizer_closure centralizer_eq_iInf
center_eq_infi' 📖	mathematical	closure Top.top AddSubgroup instTop	center iInf Set.Elem instInfSet centralizer Set Set.instSingletonSet Set.instMembership	—	center_eq_iInf iInf_subtype''
center_le_centralizer 📖	mathematical	—	AddSubgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder center centralizer	—	Set.addCenter_subset_addCentralizer
centralizer_closure 📖	mathematical	—	centralizer SetLike.coe AddSubgroup instSetLike closure	—	le_antisymm centralizer_le subset_closure le_centralizer_iff closure_le_centralizer_centralizer
centralizer_eq_iInf 📖	mathematical	—	centralizer iInf AddSubgroup instInfSet Set Set.instMembership Set.instSingletonSet	—	le_antisymm le_iInf₂ centralizer_le Set.singleton_subset_iff mem_iInf mem_centralizer_singleton_iff
centralizer_eq_top_iff_subset 📖	mathematical	—	centralizer Top.top AddSubgroup instTop Set Set.instHasSubset SetLike.coe instSetLike center	—	SetLike.ext'_iff Set.addCentralizer_eq_top_iff_subset
centralizer_le 📖	mathematical	Set Set.instHasSubset	AddSubgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder centralizer	—	AddSubmonoid.centralizer_le
centralizer_univ 📖	mathematical	—	centralizer Set.univ center	—	SetLike.ext' Set.addCentralizer_univ
characteristic_centralizer 📖	mathematical	—	Characteristic centralizer SetLike.coe AddSubgroup instSetLike	—	characteristic_iff_comap_le AddEquiv.injective map_add AddMonoidHomClass.toAddHomClass AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass characteristic_iff_le_comap
closure_le_centralizer_centralizer 📖	mathematical	—	AddSubgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder closure centralizer SetLike.coe instSetLike	—	closure_le Set.subset_addCentralizer_addCentralizer
le_centralizer 📖	mathematical	—	AddSubgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder centralizer SetLike.coe instSetLike	—	le_centralizer_iff_isAddCommutative
le_centralizer_iff 📖	mathematical	—	AddSubgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder centralizer SetLike.coe instSetLike	—	—
le_centralizer_iff_isAddCommutative 📖	mathematical	—	AddSubgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder centralizer SetLike.coe instSetLike IsAddCommutative SetLike.instMembership add	—	IsAddCommutative.is_comm
map_centralizer_le_centralizer_image 📖	mathematical	—	AddSubgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder map centralizer Set.image DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddMonoidHom.instFunLike	—	map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass
mem_centralizer_iff 📖	mathematical	—	AddSubgroup SetLike.instMembership instSetLike centralizer AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	—
mem_centralizer_iff_commutator_eq_zero 📖	mathematical	—	AddSubgroup SetLike.instMembership instSetLike centralizer AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid NegZeroClass.toZero	—	mem_centralizer_iff add_neg_eq_iff_eq_add zero_add
mem_centralizer_singleton_iff 📖	mathematical	—	AddSubgroup SetLike.instMembership instSetLike centralizer Set Set.instSingletonSet AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	mem_centralizer_iff Set.mem_singleton_iff
normal_centralizer 📖	mathematical	—	Normal centralizer SetLike.coe AddSubgroup instSetLike	—	add_assoc neg_neg add_neg_cancel_left add_neg_cancel add_zero Normal.conj_mem

Subgroup

Definitions

Name	Category	Theorems
centralizer 📖	CompOp	45 math math: mem_centralizer_iff_commutator_eq_one, characteristic_centralizer, Equiv.Perm.Basis.toCentralizer_equivariant, ConjAct.stabilizer_eq_centralizer, centralizer_univ, Equiv.Perm.Basis.toCentralizer_apply, Equiv.Perm.OnCycleFactors.mem_range_toPermHom_iff', le_centralizer_iff, mem_centralizer_iff, Equiv.Perm.OnCycleFactors.nat_card_range_toPermHom, quotientCentralizerEmbedding_apply, le_centralizer, centralizer_eq_top_iff_subset, normalizerMonoidHom_ker, centralizer_closure, Equiv.Perm.Basis.ofPermHom_mem_centralizer, Sylow.normalizer_le_centralizer_or_le_commutator, Equiv.Perm.OnCycleFactors.val_centralizer_smul, commutator_eq_bot_iff_le_centralizer, map_centralizer_le_centralizer_image, Equiv.Perm.Basis.toPermHom_apply_toCentralizer, Equiv.Perm.centralizer_le_alternating_iff, mem_centralizer_singleton_iff, Equiv.Perm.OnCycleFactors.mem_ker_toPermHom_iff, closure_le_centralizer_centralizer, commutator_centralizer_commutator_le_center, Equiv.Perm.OnCycleFactors.coe_toPermHom, center_le_centralizer, Equiv.Perm.OnCycleFactors.mem_range_toPermHom_iff, centralizer_le, Equiv.Perm.OnCycleFactors.kerParam_range_eq_centralizer_of_count_le_one, Equiv.Perm.OnCycleFactors.toPermHom_apply, center_eq_infi', center_eq_iInf, Equiv.Perm.OnCycleFactors.kerParam_range_le_centralizer, le_centralizer_iff_isMulCommutative, Equiv.Perm.OnCycleFactors.kerParam_range_eq, IsCyclic.normalizer_le_centralizer, nat_card_centralizer_nat_card_stabilizer, Equiv.Perm.nat_card_centralizer, normal_centralizer, Equiv.Perm.OnCycleFactors.range_toPermHom_eq_range_toPermHom', Equiv.Perm.OnCycleFactors.centralizer_smul_def, centralizer_eq_comap_stabilizer, centralizer_eq_iInf
closureCommGroupOfComm 📖	CompOp	—
instMulDistribMulActionSubtypeMemNormalizer 📖	CompOp	1 math math: smul_coe
normalizerMonoidHom 📖	CompOp	6 math math: normalizerMonoidHom_ker, normalizerMonoidHom_apply_apply_coe, SemidirectProduct.mulEquivSubgroup_apply, SemidirectProduct.mulEquivSubgroup_symm_apply, normalizerMonoidHom_apply_symm_apply_coe, SemidirectProduct.monoidHomSubgroup_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
center_eq_iInf 📖	mathematical	closure Top.top Subgroup instTop	center iInf instInfSet Set Set.instMembership centralizer Set.instSingletonSet	—	centralizer_univ coe_top centralizer_closure centralizer_eq_iInf
center_eq_infi' 📖	mathematical	closure Top.top Subgroup instTop	center iInf Set.Elem instInfSet centralizer Set Set.instSingletonSet Set.instMembership	—	center_eq_iInf iInf_subtype''
center_le_centralizer 📖	mathematical	—	Subgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder center centralizer	—	Set.center_subset_centralizer
centralizer_closure 📖	mathematical	—	centralizer SetLike.coe Subgroup instSetLike closure	—	le_antisymm centralizer_le subset_closure le_centralizer_iff closure_le_centralizer_centralizer
centralizer_eq_iInf 📖	mathematical	—	centralizer iInf Subgroup instInfSet Set Set.instMembership Set.instSingletonSet	—	le_antisymm le_iInf₂ centralizer_le Set.singleton_subset_iff
centralizer_eq_top_iff_subset 📖	mathematical	—	centralizer Top.top Subgroup instTop Set Set.instHasSubset SetLike.coe instSetLike center	—	SetLike.ext'_iff Set.centralizer_eq_top_iff_subset
centralizer_le 📖	mathematical	Set Set.instHasSubset	Subgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder centralizer	—	Submonoid.centralizer_le
centralizer_univ 📖	mathematical	—	centralizer Set.univ center	—	SetLike.ext' Set.centralizer_univ
characteristic_centralizer 📖	mathematical	—	Characteristic centralizer SetLike.coe Subgroup instSetLike	—	characteristic_iff_comap_le MulEquiv.injective map_mul MonoidHomClass.toMulHomClass MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass characteristic_iff_le_comap
closure_le_centralizer_centralizer 📖	mathematical	—	Subgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder closure centralizer SetLike.coe instSetLike	—	closure_le Set.subset_centralizer_centralizer
le_centralizer 📖	mathematical	—	Subgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder centralizer SetLike.coe instSetLike	—	le_centralizer_iff_isMulCommutative
le_centralizer_iff 📖	mathematical	—	Subgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder centralizer SetLike.coe instSetLike	—	—
le_centralizer_iff_isMulCommutative 📖	mathematical	—	Subgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder centralizer SetLike.coe instSetLike IsMulCommutative SetLike.instMembership mul	—	IsMulCommutative.is_comm
map_centralizer_le_centralizer_image 📖	mathematical	—	Subgroup Preorder.toLE PartialOrder.toPreorder instPartialOrder map centralizer Set.image DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike	—	map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass
mem_centralizer_iff 📖	mathematical	—	Subgroup SetLike.instMembership instSetLike centralizer MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	—
mem_centralizer_iff_commutator_eq_one 📖	mathematical	—	Subgroup SetLike.instMembership instSetLike centralizer MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid InvOneClass.toOne	—	one_mul
mem_centralizer_singleton_iff 📖	mathematical	—	Subgroup SetLike.instMembership instSetLike centralizer Set Set.instSingletonSet MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	—
normal_centralizer 📖	mathematical	—	Normal centralizer SetLike.coe Subgroup instSetLike	—	mul_assoc inv_inv mul_inv_cancel_left mul_inv_cancel mul_one Normal.conj_mem
normalizerMonoidHom_apply_apply_coe 📖	mathematical	—	Subgroup SetLike.instMembership instSetLike DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid toGroup EquivLike.toFunLike MulEquiv.instEquivLike MonoidHom normalizer MulAut mul MulAut.instGroup MonoidHom.instFunLike normalizerMonoidHom InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
normalizerMonoidHom_apply_symm_apply_coe 📖	mathematical	—	Subgroup SetLike.instMembership instSetLike DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid toGroup EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm MonoidHom normalizer MulAut mul MulAut.instGroup MonoidHom.instFunLike normalizerMonoidHom InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	inv_inv
normalizerMonoidHom_ker 📖	mathematical	—	MonoidHom.ker Subgroup SetLike.instMembership instSetLike normalizer toGroup MulAut mul Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MulAut.instGroup normalizerMonoidHom subgroupOf centralizer SetLike.coe	—	—
smul_coe 📖	mathematical	—	Subgroup SetLike.instMembership instSetLike normalizer SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toGroup MulAction.toSemigroupAction MulDistribMulAction.toMulAction instMulDistribMulActionSubtypeMemNormalizer MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass inv	—	—

---

← Back to Index