FixedPoints

📁 Source: Mathlib/GroupTheory/GroupAction/FixedPoints.lean

Statistics

Metric	Count
Definitions	0
Theorems fixedBy_add, fixedBy_eq_univ_iff_eq_zero, fixedBy_mem_fixedBy_of_addCommute, fixedBy_neg, fixedBy_subset_fixedBy_zsmul, fixedBy_zero_eq_univ, mem_fixedBy_zmultiples_iff_mem_fixedBy, mem_fixedBy_zsmul, minimalPeriod_eq_one_iff_fixedBy, movedBy_mem_fixedBy_of_addCommute, not_addCommute_of_disjoint_movedBy_preimage, set_mem_fixedBy_iff, set_mem_fixedBy_of_movedBy_subset, set_mem_fixedBy_of_subset_fixedBy, vadd_fixedBy, vadd_mem_fixedBy_iff_mem_fixedBy, vadd_mem_of_set_mem_fixedBy, vadd_neg_mem_fixedBy_iff_mem_fixedBy, vadd_zsmul_fixedBy_eq_of_addCommute, vadd_zsmul_movedBy_eq_of_addCommute, map_mem_fixedBy, map_mem_fixedPoints, fixedBy_eq_univ_iff_eq_one, fixedBy_inv, fixedBy_mem_fixedBy_of_commute, fixedBy_mul, fixedBy_one_eq_univ, fixedBy_subset_fixedBy_zpow, mem_fixedBy_zpow, mem_fixedBy_zpowers_iff_mem_fixedBy, minimalPeriod_eq_one_iff_fixedBy, movedBy_mem_fixedBy_of_commute, not_commute_of_disjoint_movedBy_preimage, set_mem_fixedBy_iff, set_mem_fixedBy_of_movedBy_subset, set_mem_fixedBy_of_subset_fixedBy, smul_fixedBy, smul_inv_mem_fixedBy_iff_mem_fixedBy, smul_mem_fixedBy_iff_mem_fixedBy, smul_mem_of_set_mem_fixedBy, smul_subset_of_set_mem_fixedBy, smul_zpow_fixedBy_eq_of_commute, smul_zpow_movedBy_eq_of_commute, map_mem_fixedBy, map_mem_fixedPoints	45
Total	45

AddAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fixedBy_add 📖	mathematical	—	Set Set.instHasSubset Set.instInter fixedBy AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	mem_fixedBy AddSemigroupAction.add_vadd
fixedBy_eq_univ_iff_eq_zero 📖	mathematical	—	fixedBy Set.univ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	vadd_left_injective' Set.eq_univ_iff_forall zero_vadd mem_fixedBy
fixedBy_mem_fixedBy_of_addCommute 📖	mathematical	AddCommute AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	Set Set.instMembership fixedBy Set.addActionSet	—	Set.ext Set.mem_vadd_set_iff_neg_vadd_mem mem_fixedBy AddSemigroupAction.add_vadd AddCommute.neg_right vadd_left_cancel_iff
fixedBy_neg 📖	mathematical	—	fixedBy SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	Set.ext mem_fixedBy neg_vadd_eq_iff
fixedBy_subset_fixedBy_zsmul 📖	mathematical	—	Set Set.instHasSubset fixedBy SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SubNegMonoid.toZSMul	—	mem_fixedBy_zsmul
fixedBy_zero_eq_univ 📖	mathematical	—	fixedBy AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass Set.univ	—	Set.eq_univ_iff_forall zero_vadd
mem_fixedBy_zmultiples_iff_mem_fixedBy 📖	mathematical	—	Set Set.instMembership fixedBy SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SubNegMonoid.toZSMul	—	mem_fixedBy one_zsmul mem_fixedBy_zsmul
mem_fixedBy_zsmul 📖	mathematical	Set Set.instMembership fixedBy SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	SubNegMonoid.toZSMul	—	mem_fixedBy zsmul_vadd_eq_iff_minimalPeriod_dvd minimalPeriod_eq_one_iff_fixedBy one_dvd
minimalPeriod_eq_one_iff_fixedBy 📖	mathematical	—	Function.minimalPeriod HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddSemigroupAction Set Set.instMembership fixedBy	—	Function.minimalPeriod_eq_one_iff_isFixedPt
movedBy_mem_fixedBy_of_addCommute 📖	mathematical	AddCommute AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	Set Set.instMembership fixedBy Set.addActionSet Compl.compl Set.instCompl	—	mem_fixedBy Set.vadd_set_compl fixedBy_mem_fixedBy_of_addCommute
not_addCommute_of_disjoint_movedBy_preimage 📖	mathematical	Disjoint Set CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Compl.compl Set.instCompl fixedBy SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid HVAdd.hVAdd instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction	AddCommute AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	Mathlib.Tactic.Contrapose.contrapose₄ fixedBy_eq_univ_iff_eq_zero compl_inj_iff Set.compl_univ Set.bot_eq_empty disjoint_self movedBy_mem_fixedBy_of_addCommute
set_mem_fixedBy_iff 📖	mathematical	—	Set Set.instMembership fixedBy SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Set.addActionSet HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction	—	mem_fixedBy eq_neg_vadd_iff Set.ext_iff Set.mem_neg_vadd_set_iff
set_mem_fixedBy_of_movedBy_subset 📖	mathematical	Set Set.instHasSubset Compl.compl Set.instCompl fixedBy SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	Set.instMembership Set.addActionSet	—	fixedBy_neg Set.ext Set.mem_neg_vadd_set_iff Set.mem_compl_iff vadd_mem_fixedBy_iff_mem_fixedBy
set_mem_fixedBy_of_subset_fixedBy 📖	mathematical	Set Set.instHasSubset fixedBy SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	Set.instMembership Set.addActionSet	—	fixedBy_neg Set.ext Set.mem_neg_vadd_set_iff neg_vadd_vadd
vadd_fixedBy 📖	mathematical	—	HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid toAddSemigroupAction fixedBy AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	Set.ext Set.mem_vadd_set_iff_neg_vadd_mem mem_fixedBy AddSemigroupAction.add_vadd vadd_eq_iff_eq_neg_vadd
vadd_mem_fixedBy_iff_mem_fixedBy 📖	mathematical	—	Set Set.instMembership fixedBy SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction	—	mem_fixedBy vadd_left_cancel_iff
vadd_mem_of_set_mem_fixedBy 📖	mathematical	Set Set.instMembership fixedBy SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Set.addActionSet	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction	—	set_mem_fixedBy_iff
vadd_neg_mem_fixedBy_iff_mem_fixedBy 📖	mathematical	—	Set Set.instMembership fixedBy SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	fixedBy_neg vadd_mem_fixedBy_iff_mem_fixedBy
vadd_zsmul_fixedBy_eq_of_addCommute 📖	mathematical	AddCommute AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction SubNegMonoid.toZSMul fixedBy	—	fixedBy_subset_fixedBy_zsmul fixedBy_mem_fixedBy_of_addCommute
vadd_zsmul_movedBy_eq_of_addCommute 📖	mathematical	AddCommute AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	HVAdd.hVAdd Set instHVAdd Set.vaddSet AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction SubNegMonoid.toZSMul Compl.compl Set.instCompl fixedBy	—	fixedBy_subset_fixedBy_zsmul movedBy_mem_fixedBy_of_addCommute

AddActionHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_mem_fixedBy 📖	mathematical	Set Set.instMembership AddAction.fixedBy	DFunLike.coe AddActionHom AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction instFunLikeAddActionHom	—	AddAction.mem_fixedBy map_vadd instAddActionSemiHomClassAddActionHom
map_mem_fixedPoints 📖	mathematical	Set Set.instMembership AddAction.fixedPoints AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.toAddMonoid AddSubmonoid.addAction	DFunLike.coe AddActionHom AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction instFunLikeAddActionHom	—	map_vadd AddAction.mem_fixedPoints

MulAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fixedBy_eq_univ_iff_eq_one 📖	mathematical	—	fixedBy Set.univ MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	smul_left_injective' Set.eq_univ_iff_forall one_smul
fixedBy_inv 📖	mathematical	—	fixedBy DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Set.ext mem_fixedBy inv_smul_eq_iff
fixedBy_mem_fixedBy_of_commute 📖	mathematical	Commute MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	Set Set.instMembership fixedBy Set.mulActionSet	—	Set.ext Set.mem_smul_set_iff_inv_smul_mem mem_fixedBy SemigroupAction.mul_smul Commute.inv_right smul_left_cancel_iff
fixedBy_mul 📖	mathematical	—	Set Set.instHasSubset Set.instInter fixedBy MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	mem_fixedBy SemigroupAction.mul_smul
fixedBy_one_eq_univ 📖	mathematical	—	fixedBy MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass Set.univ	—	Set.eq_univ_iff_forall one_smul
fixedBy_subset_fixedBy_zpow 📖	mathematical	—	Set Set.instHasSubset fixedBy DivInvMonoid.toMonoid Group.toDivInvMonoid DivInvMonoid.toZPow	—	mem_fixedBy_zpow
mem_fixedBy_zpow 📖	mathematical	Set Set.instMembership fixedBy DivInvMonoid.toMonoid Group.toDivInvMonoid	DivInvMonoid.toZPow	—	mem_fixedBy zpow_smul_eq_iff_minimalPeriod_dvd minimalPeriod_eq_one_iff_fixedBy one_dvd
mem_fixedBy_zpowers_iff_mem_fixedBy 📖	mathematical	—	Set Set.instMembership fixedBy DivInvMonoid.toMonoid Group.toDivInvMonoid DivInvMonoid.toZPow	—	zpow_one mem_fixedBy_zpow
minimalPeriod_eq_one_iff_fixedBy 📖	mathematical	—	Function.minimalPeriod SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toSemigroupAction Set Set.instMembership fixedBy	—	Function.minimalPeriod_eq_one_iff_isFixedPt
movedBy_mem_fixedBy_of_commute 📖	mathematical	Commute MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	Set Set.instMembership fixedBy Set.mulActionSet Compl.compl Set.instCompl	—	mem_fixedBy Set.smul_set_compl fixedBy_mem_fixedBy_of_commute
not_commute_of_disjoint_movedBy_preimage 📖	mathematical	Disjoint Set CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Compl.compl Set.instCompl fixedBy DivInvMonoid.toMonoid Group.toDivInvMonoid Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction	Commute MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	Mathlib.Tactic.Contrapose.contrapose₄ fixedBy_eq_univ_iff_eq_one compl_inj_iff Set.compl_univ Set.bot_eq_empty disjoint_self movedBy_mem_fixedBy_of_commute
set_mem_fixedBy_iff 📖	mathematical	—	Set Set.instMembership fixedBy DivInvMonoid.toMonoid Group.toDivInvMonoid Set.mulActionSet SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction	—	—
set_mem_fixedBy_of_movedBy_subset 📖	mathematical	Set Set.instHasSubset Compl.compl Set.instCompl fixedBy DivInvMonoid.toMonoid Group.toDivInvMonoid	Set.instMembership Set.mulActionSet	—	fixedBy_inv Set.ext Set.mem_inv_smul_set_iff Set.mem_compl_iff smul_mem_fixedBy_iff_mem_fixedBy
set_mem_fixedBy_of_subset_fixedBy 📖	mathematical	Set Set.instHasSubset fixedBy DivInvMonoid.toMonoid Group.toDivInvMonoid	Set.instMembership Set.mulActionSet	—	fixedBy_inv Set.ext Set.mem_inv_smul_set_iff inv_smul_smul
smul_fixedBy 📖	mathematical	—	Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid toSemigroupAction fixedBy MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Set.ext SemigroupAction.mul_smul smul_eq_iff_eq_inv_smul
smul_inv_mem_fixedBy_iff_mem_fixedBy 📖	mathematical	—	Set Set.instMembership fixedBy DivInvMonoid.toMonoid Group.toDivInvMonoid SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	fixedBy_inv smul_mem_fixedBy_iff_mem_fixedBy
smul_mem_fixedBy_iff_mem_fixedBy 📖	mathematical	—	Set Set.instMembership fixedBy DivInvMonoid.toMonoid Group.toDivInvMonoid SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction	—	mem_fixedBy smul_left_cancel_iff
smul_mem_of_set_mem_fixedBy 📖	mathematical	Set Set.instMembership fixedBy DivInvMonoid.toMonoid Group.toDivInvMonoid Set.mulActionSet	SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction	—	set_mem_fixedBy_iff
smul_subset_of_set_mem_fixedBy 📖	mathematical	Set Set.instHasSubset Set.instMembership fixedBy DivInvMonoid.toMonoid Group.toDivInvMonoid Set.mulActionSet	Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction	—	HasSubset.Subset.trans Set.instIsTransSubset Set.smul_set_subset_smul_set_iff Eq.subset Set.instReflSubset
smul_zpow_fixedBy_eq_of_commute 📖	mathematical	Commute MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction DivInvMonoid.toZPow fixedBy	—	fixedBy_subset_fixedBy_zpow fixedBy_mem_fixedBy_of_commute
smul_zpow_movedBy_eq_of_commute 📖	mathematical	Commute MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	Set Set.smulSet SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction DivInvMonoid.toZPow Compl.compl Set.instCompl fixedBy	—	fixedBy_subset_fixedBy_zpow movedBy_mem_fixedBy_of_commute

MulActionHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_mem_fixedBy 📖	mathematical	Set Set.instMembership MulAction.fixedBy	DFunLike.coe MulActionHom SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction instFunLikeMulActionHom	—	map_smul instMulActionSemiHomClassMulActionHom
map_mem_fixedPoints 📖	mathematical	Set Set.instMembership MulAction.fixedPoints Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.toMonoid Submonoid.mulAction	DFunLike.coe MulActionHom SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction instFunLikeMulActionHom	—	map_smul

---

← Back to Index