| Name | Category | Theorems |
|---|
fixedBy 📖 | CompOp | 20 mathmath: fixedBy_neg, movedBy_mem_fixedBy_of_addCommute, vadd_neg_mem_fixedBy_iff_mem_fixedBy, mem_fixingAddSubgroup_compl_iff_movedBy_subset, vadd_fixedBy, fixedBy_subset_fixedBy_zsmul, mem_fixedBy_zmultiples_iff_mem_fixedBy, fixedBy_zero_eq_univ, vadd_zsmul_movedBy_eq_of_addCommute, vadd_zsmul_fixedBy_eq_of_addCommute, mem_fixedBy, fixed_eq_iInter_fixedBy, sum_card_fixedBy_eq_card_orbits_mul_card_addGroup, minimalPeriod_eq_one_iff_fixedBy, set_mem_fixedBy_iff, vadd_mem_fixedBy_iff_mem_fixedBy, fixedBy_mem_fixedBy_of_addCommute, mem_fixingAddSubgroup_iff_subset_fixedBy, fixedBy_eq_univ_iff_eq_zero, fixedBy_add
|
fixedPoints 📖 | CompOp | 14 mathmath: fixedPoints_addSubmonoid_iSup, fixingAddSubmonoid_fixedPoints_gc, fixedPoints_addSubmonoid_sup, fixedPoints_addSubgroup_antitone, fixed_eq_iInter_fixedBy, fixedPoints_antitone_addSubmonoid, fixingAddSubgroup_fixedPoints_gc, fixedPoints_addSubgroup_iSup, mem_fixedPoints', fixedPoints_addSubgroup_sup, mem_fixedPoints, mem_fixedPoints_iff_card_orbit_eq_one, subsingleton_orbit_iff_mem_fixedPoints, fixedPoints_of_subsingleton
|
instAddAction 📖 | CompOp | 38 mathmath: mem_addSubgroup_orbit_iff, AddCircle.isAddFundamentalDomain_of_ae_ball, finite_quotient_of_finite_quotient_of_finite_quotient, Circle.isAddQuotientCoveringMap_exp, orbit_fixingAddSubgroup_compl_subset, orbitZMultiplesEquiv_symm_apply', orbitZMultiplesEquiv_symm_apply, MeasureTheory.Measure.IsAddLeftInvariant.addQuotientMeasureEqMeasurePreimage_of_set, isAddFundamentalDomain_Ioc, orbit_addSubgroup_eq_self_of_mem, zmultiplesQuotientStabilizerEquiv_symm_apply, finite_quotient_of_pretransitive_of_finite_quotient, minimalPeriod_eq_card, AddSubgroup.continuousVAdd, orbitRel_addSubgroup_le, Complex.isAddQuotientCoveringMap_exp, fixedPoints_addSubgroup_antitone, ZSpan.isAddFundamentalDomain', Function.Periodic.map_vadd_zmultiples, instProperVAddSubtypeMemAddSubgroupOfIsClosedCoe, addSubgroup_vadd_def, orbit_addSubgroup_zero_eq_self, IsFundamentalDomain.AddQuotientMeasureEqMeasurePreimage_AddHaarMeasure, AddCircle.instAddQuotientMeasureEqMeasurePreimageSubtypeAddOppositeRealMemAddSubgroupOpZmultiplesVolume, QuotientAddGroup.orbit_eq_out_vadd, right_quotientAction, fixingAddSubgroup_fixedPoints_gc, fixedPoints_addSubgroup_iSup, orbit_addSubgroup_subset, orbit_addSubgroup_eq_rightCoset, fixedPoints_addSubgroup_sup, instProperVAddSubtypeAddOppositeMemAddSubgroupOpOfIsTopologicalAddGroupOfIsClosedCoe, orbitRel.Quotient.mem_addSubgroup_orbit_iff, orbitRel_addSubgroupOf, QuotientAddGroup.orbit_mk_eq_vadd, orbitRel.Quotient.addSubgroup_quotient_eq_iff, MeasureTheory.leftInvariantIsAddQuotientMeasureEqMeasurePreimage, IsFundamentalDomain.AddQuotientMeasureEqMeasurePreimage_vaddAddHaarMeasure
|
instDecidablePredMemAddSubgroupStabilizerOfDecidableEq 📖 | CompOp | — |
instDecidablePredMemAddSubmonoidStabilizerAddSubmonoidOfDecidableEq 📖 | CompOp | — |
instElemOrbit 📖 | CompOp | 5 mathmath: mem_addSubgroup_orbit_iff, orbitZMultiplesEquiv_symm_apply', orbitZMultiplesEquiv_symm_apply, orbit.coe_vadd, instIsPretransitiveElemOrbit
|
instElemOrbit_1 📖 | CompOp | 4 mathmath: orbitRel.Quotient.orbit.coe_vadd, instIsPretransitiveElemOrbit_1, orbitRel.Quotient.mem_addSubgroup_orbit_iff, orbitRel.Quotient.addSubgroup_quotient_eq_iff
|
orbit 📖 | CompOp | 60 mathmath: orbit_eq_iff, isAddQuotientCoveringMap_iff_isCoveringMap_and, mem_addSubgroup_orbit_iff, nonempty_orbit, mapsTo_vadd_orbit, orbitRel_apply, IsBlock.ncard_block_add_ncard_orbit_eq, orbit.pairwiseDisjoint, orbit_fixingAddSubgroup_compl_subset, orbitZMultiplesEquiv_symm_apply', IsBlock.of_orbit, orbitZMultiplesEquiv_symm_apply, mem_orbit_vadd, orbit_addSubgroup_eq_self_of_mem, IsAddQuotientCoveringMap.apply_eq_iff_mem_orbit, SubAddAction.val_image_orbit, orbit.coe_vadd, isPretransitive_iff_orbit_eq_univ, mem_orbit_self, vadd_orbit_eq_orbit_vadd, vadd_orbit, minimalPeriod_eq_card, vadd_orbit_subset, Finite.finite_addAction_orbit, orbit_addSubmonoid_subset, mem_orbit_iff, IsFixedBlock.orbit, IsMinimal.dense_orbit, IsBlock.orbit, orbitRel.Quotient.mem_addSubgroup_orbit_iff', SubAddAction.val_preimage_orbit, mem_orbit, orbitEquivQuotientStabilizer_symm_apply, SubAddAction.mem_orbit_subAdd_iff, dense_orbit, card_orbit_mul_card_stabilizer_eq_card_addGroup, orbit.eq_or_disjoint, orbit_addSubgroup_zero_eq_self, orbit_eq_univ, IsBlock.orbit_stabilizer_eq, vadd_closure_orbit_subset, ofQuotientStabilizer_mem_orbit, instIsPretransitiveElemOrbit, IsPartition.of_orbits, orbit_addSubgroup_subset, orbit_addSubgroup_eq_rightCoset, mem_fixedPoints_iff_card_orbit_eq_one, orbit_vadd, orbitRel.Quotient.orbit_eq_orbit_out, stabilizer_orbit_eq, orbitRel.Quotient.mem_addSubgroup_orbit_iff, subsingleton_orbit_iff_mem_fixedPoints, index_stabilizer, orbitRel.Quotient.orbit_mk, isAddQuotientCoveringMap_iff, vadd_mem_orbit_vadd, mem_orbit_symm, IsBlock.orbit_of_normal, orbit_vadd_subset, IsBlockSystem.of_normal
|
orbitRel 📖 | CompOp | 32 mathmath: isOpenMap_quotient_mk'_add, orbitRel_apply, MeasureTheory.instSigmaFiniteAddQuotientOrbitRelInstMeasurableSpaceToMeasurableSpace, MeasureTheory.IsAddFundamentalDomain.addQuotientMeasure_eq, MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addProjection_respects_measure', orbitRel_le_fst, MeasureTheory.IsAddFundamentalDomain.measurePreserving_add_quotient_mk, isClosedMap_quotient, isAddQuotientCoveringMap_quotientMk_of_properlyDiscontinuousVAdd, image_inter_image_iff, isOpenQuotientMap_quotientMk, ContinuousConstVAdd.secondCountableTopology, t2Space_quotient_addAction_of_properVAdd, orbitRel_addSubgroup_le, t2Space_of_properlyDiscontinuousVAdd_of_t2Space, orbitRel.Quotient.mem_orbit, orbitRel_le_snd, quotient_preimage_image_eq_union_add, MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage_of_zero, isCoveringMapOn_quotientMk_of_properlyDiscontinuousVAdd, SubAddAction.orbitRel_of_subAdd, sum_card_fixedBy_eq_card_orbits_mul_card_addGroup, automorphize_smul_left, MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage_addQuotientMeasure, MeasureTheory.AddQuotientMeasureEqMeasurePreimage.isFiniteMeasure_quotient, disjoint_image_image_iff, MeasureTheory.AddQuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient, card_eq_sum_card_addGroup_sub_card_stabilizer, MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure, orbitRel.Quotient.orbit_mk, orbitRel_addSubgroupOf, orbitRel.Quotient.addSubgroup_quotient_eq_iff
|
selfEquivSigmaOrbits 📖 | CompOp | — |
selfEquivSigmaOrbits' 📖 | CompOp | — |
stabilizer 📖 | CompOp | 99 mathmath: mem_stabilizer_set_iff_subset_vadd_set, stabilizer_addSubgroup_op, SubAddAction.notMem_val_image, stabilizerEquivStabilizer_symm, SubAddAction.ofStabilizer.conjMap_comp, SubAddAction.ofFixingAddSubgroup_of_singleton_bijective, stabilizer_vadd_eq_stabilizer_map_conj, stabilizer_add_eq_left, SubAddAction.mem_ofStabilizer_iff, stabilizer_inf_stabilizer_le_stabilizer_apply₂, SubAddAction.ofStabilizer.isMultiplyPretransitive_iff_of_conj, stabilizer_singleton, injective_ofQuotientStabilizer, map_stabilizer_le, Finset.op_vadd_stabilizer_of_no_doubling, SubAddAction.ofStabilizer.conjMap_comp_neg_apply, stabilizer_le_aestabilizer, mem_stabilizer_iff, stabilizer_finset_univ, stabilizer_univ, SubAddAction.ofStabilizer.isPretransitive_iff, ProperlyDiscontinuousVAdd.finite_stabilizer, stabilizer_empty, stabilizer_add_self, stabilizer_vadd_eq_right, Set.powersetCard.addAction_stabilizer_coe, IsBlock.stabilizer_le, stabilizer_op_addSubgroup, Topology.IsQuotientMap.isCoveringMapOn_of_properlyDiscontinuousVAdd, zmultiplesQuotientStabilizerEquiv_symm_apply, stabilizerEquivStabilizer_symm_apply, stabilizer_vadd_eq_left, SubAddAction.ofFixingAddSubgroup_insert_map_bijective, stabilizer_finset_singleton, SubAddAction.nat_card_ofStabilizer_eq, fixingAddSubgroup_le_stabilizer, stabilizerEquivStabilizer_neg, mem_stabilizer_finset', stabilizer_inf_stabilizer_le_stabilizer_inter, mem_stabilizer_set', SubAddAction.ofStabilizer.isMultiplyPretransitive_iff, le_stabilizer_vadd_right, op_vadd_set_stabilizer_subset, index_stabilizer_of_transitive, SubAddAction.ofStabilizer.conjMap_bijective, stabilizer_inf_stabilizer_le_stabilizer_union, isCancelVAdd_iff_stabilizer_eq_bot, orbitEquivQuotientStabilizer_symm_apply, card_orbit_mul_card_stabilizer_eq_card_addGroup, isMultiplyPreprimitive_succ_iff_ofStabilizer, SubAddAction.ofStabilizer.snoc_castSucc, mem_stabilizer_finset_iff_subset_vadd_finset, SubAddAction.ENat_card_ofStabilizer_add_zero_eq, isCoveringMapOn_quotientMk_of_properlyDiscontinuousVAdd, SubAddAction.fixingAddSubgroup_of_insert, stabilizerEquivStabilizer_apply, stabilizer_coe_finset, IsBlock.orbit_stabilizer_eq, stabilizerEquivStabilizer_trans, stabilizer_addSubgroup, SubAddAction.ofStabilizer.neg_conjMap_comp_apply, Finset.vadd_stabilizer_of_no_doubling, stabilizer_image_coe_quotient, mem_stabilizer_finset, stabilizer_finite, mem_stabilizer_set_iff_vadd_set_subset, add_stabilizer_self, SubAddAction.nat_card_ofStabilizer_add_zero_eq, card_eq_sum_card_addGroup_sub_card_stabilizer, SubAddAction.ofStabilizer_carrier, stabilizer_finset_empty, card_eq_sum_card_addGroup_sub_card_stabilizer', stabilizer_subset_sub_right, SubAddAction.ofStabilizer.conjMap_comp_apply, SubAddAction.ofStabilizer.isMultiplyPretransitive, le_stabilizer_iff_vadd_le, Topology.IsQuotientMap.isCoveringMapOn_of_vadd_disjoint, mem_stabilizer_set, stabilizer_inf_stabilizer_le_stabilizer_sdiff, stabilizerEquivStabilizer_zero, stabilizer_add_eq_right, le_stabilizer_vadd_left, stabilizerEquivStabilizer_compTriple, IsBlock.ncard_block_eq_relIndex, ofQuotientStabilizer_vadd, SubAddAction.stabilizer_of_subAdd, index_stabilizer, isPreprimitive_fixingAddSubgroup_insert_iff, IsCancelVAdd.stabilizer_eq_bot, isMultiplyPreprimitive_ofStabilizer, vadd_set_stabilizer_subset, SubAddAction.mem_ofFixingAddSubgroup_insert_iff, ofQuotientStabilizer_mk, isCoatom_stabilizer_iff_preprimitive, IsPreprimitive.isCoatom_stabilizer_of_isPreprimitive, mem_stabilizer_finset_iff_vadd_finset_subset, stabilizer_quotient, SubAddAction.ofStabilizer.isPretransitive_iff_of_conj, SubAddAction.ofStabilizer.conjMap_apply
|
stabilizerAddSubmonoid 📖 | CompOp | 2 mathmath: SubAddAction.stabilizer_of_subMul.addSubmonoid, mem_stabilizerAddSubmonoid_iff
|
| Name | Category | Theorems |
|---|
fixedBy 📖 | CompOp | 25 mathmath: set_mem_fixedBy_iff, smul_zpow_movedBy_eq_of_commute, fixed_eq_iInter_fixedBy, sum_card_fixedBy_eq_card_orbits_mul_card_group, minimalPeriod_eq_one_iff_fixedBy, mem_closure_isSwap, smul_inv_mem_fixedBy_iff_mem_fixedBy, finite_compl_fixedBy_swap, Equiv.Perm.IsSwap.finite_compl_fixedBy, fixedBy_mul, mem_fixingSubgroup_compl_iff_movedBy_subset, smul_fixedBy, fixedBy_one_eq_univ, finite_compl_fixedBy_closure_iff, mem_closure_isSwap', mem_fixedBy_zpowers_iff_mem_fixedBy, fixedBy_inv, mem_fixingSubgroup_iff_subset_fixedBy, smul_mem_fixedBy_iff_mem_fixedBy, fixedBy_mem_fixedBy_of_commute, fixedBy_eq_univ_iff_eq_one, smul_zpow_fixedBy_eq_of_commute, fixedBy_subset_fixedBy_zpow, mem_fixedBy, movedBy_mem_fixedBy_of_commute
|
fixedPoints 📖 | CompOp | 27 mathmath: ConjAct.fixedPoints_eq_center, CategoryTheory.Limits.SingleObj.Types.sections.equivFixedPoints_apply_coe, fixedPoints_of_subsingleton, IsPGroup.sylow_mem_fixedPoints_iff, fixedPoints_subgroup_iSup, quotient_out_smul_fixedPoints, fixed_eq_iInter_fixedBy, fixedPoints_submonoid_sup, Subgroup.sylow_mem_fixedPoints_iff, mem_fixedPoints, coe_quotient_smul_fixedPoints, CategoryTheory.Limits.SingleObj.Types.limitEquivFixedPoints_symm_apply, IsPGroup.card_modEq_card_fixedPoints, coe_smul_fixedPoints_of_normal, fixedPoints_submonoid_iSup, mem_fixedPoints_iff_card_orbit_eq_one, CategoryTheory.Limits.SingleObj.Types.limitEquivFixedPoints_apply_coe, fixingSubmonoid_fixedPoints_gc, fixedPoints_subgroup_sup, fixedPoints_subgroup_antitone, fixingSubgroup_fixedPoints_gc, CategoryTheory.Limits.SingleObj.Types.sections.equivFixedPoints_symm_apply_coe, mem_fixedPoints', fixedPoints_antitone, subsingleton_orbit_iff_mem_fixedPoints, Sylow.mem_fixedPoints_mul_left_cosets_iff_mem_normalizer, IsPGroup.nonempty_fixed_point_of_prime_not_dvd_card
|
instDecidablePredMemSubgroupStabilizerOfDecidableEq 📖 | CompOp | — |
instDecidablePredMemSubmonoidStabilizerSubmonoidOfDecidableEq 📖 | CompOp | — |
instElemOrbit 📖 | CompOp | 5 mathmath: mem_subgroup_orbit_iff, orbitZPowersEquiv_symm_apply, instIsPretransitiveElemOrbit, orbit.coe_smul, orbitZPowersEquiv_symm_apply'
|
instElemOrbit_1 📖 | CompOp | 4 mathmath: instIsPretransitiveElemOrbit_1, orbitRel.Quotient.mem_subgroup_orbit_iff, orbitRel.Quotient.orbit.coe_smul, orbitRel.Quotient.subgroup_quotient_eq_iff
|
instMulAction 📖 | CompOp | 50 mathmath: fixedPoints_subgroup_iSup, quotient_out_smul_fixedPoints, Complex.isQuotientCoveringMap_npow, right_quotientAction, orbit_subgroup_subset, orbit_subgroup_eq_self_of_mem, alternatingGroup.isCoatom_stabilizer_singleton, orbitRel.Quotient.mem_subgroup_orbit_iff, mem_closure_isSwap, Set.powersetCard.isPretransitive_alternatingGroup, alternatingGroup.stabilizer.surjective_toPerm, Circle.isQuotientCoveringMap_zpow, isQuotientCoveringMap_npow, MeasureTheory.Measure.IsMulLeftInvariant.quotientMeasureEqMeasurePreimage_of_set, coe_quotient_smul_fixedPoints, finite_quotient_of_finite_quotient_of_finite_quotient, swap_mem_closure_isSwap, finite_quotient_of_pretransitive_of_finite_quotient, orbitRel.Quotient.subgroup_quotient_eq_iff, coe_smul_fixedPoints_of_normal, QuotientGroup.orbit_eq_out_smul, mem_subgroup_orbit_iff, orbitZPowersEquiv_symm_apply, Circle.isQuotientCoveringMap_npow, isQuotientCoveringMap_zpow, Subgroup.continuousSMul, alternatingGroup.exists_mem_stabilizer_smul_eq, orbitRel_subgroupOf, IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_HaarMeasure, zpowersQuotientStabilizerEquiv_symm_apply, orbitZPowersEquiv_symm_apply', alternatingGroup.stabilizer_isPreprimitive, cosetToCuspOrbit_apply_mk, alternatingGroup.isCoatom_stabilizer, fixedPoints_subgroup_sup, fixedPoints_subgroup_antitone, IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_smulHaarMeasure, orbitRel_subgroup_le, orbit_subgroup_eq_rightCoset, Set.powersetCard.isPreprimitive_alternatingGroup, subgroup_smul_def, instProperSMulSubtypeMulOppositeMemSubgroupOpOfIsTopologicalGroupOfIsClosedCoe, fixingSubgroup_fixedPoints_gc, QuotientGroup.orbit_mk_eq_smul, instProperSMulSubtypeMemSubgroupOfIsClosedCoe, orbit_subgroup_one_eq_self, MeasureTheory.leftInvariantIsQuotientMeasureEqMeasurePreimage, minimalPeriod_eq_card, orbit_fixingSubgroup_compl_subset, alternatingGroup.isCoatom_stabilizer_of_ncard_lt_ncard_compl
|
orbit 📖 | CompOp | 73 mathmath: nonempty_orbit, isPretransitive_iff_orbit_eq_univ, isQuotientCoveringMap_iff, ofQuotientStabilizer_mem_orbit, smul_mem_orbit_smul, RootPairing.span_orbit_eq_top, Normal.minpoly_eq_iff_mem_orbit, mem_orbit_smul, orbit_subgroup_subset, orbitRel.Quotient.mem_subgroup_orbit_iff', orbit_subgroup_eq_self_of_mem, Finite.finite_mulAction_orbit, index_stabilizer, mem_orbit_symm, orbitRel.Quotient.mem_subgroup_orbit_iff, IsBlock.orbit_of_normal, mem_closure_isSwap, mem_orbit_iff, Sylow.orbit_eq_top, smul_orbit, IsBlock.orbit_stabilizer_eq, IsQuotientCoveringMap.apply_eq_iff_mem_orbit, orbit.eq_or_disjoint, IsFixedBlock.orbit, Algebra.IsInvariant.orbit_eq_primesOver, IsPartition.of_orbits, smul_orbit_subset, isQuotientCoveringMap_iff_isCoveringMap_and, orbit_smul_subset, SubMulAction.mem_orbit_subMul_iff, SubMulAction.val_image_orbit, IsPGroup.card_orbit, dense_orbit, swap_mem_closure_isSwap, smul_closure_orbit_subset, mem_subgroup_orbit_iff, orbitRel_apply, orbitZPowersEquiv_symm_apply, instIsPretransitiveElemOrbit, orbitRel.Quotient.orbit_mk, orbitEquivQuotientStabilizer_symm_apply, mem_fixedPoints_iff_card_orbit_eq_one, orbit.coe_smul, orbitZPowersEquiv_symm_apply', Module.End.span_orbit_mem_invtSubmodule, orbit.pairwiseDisjoint, orbit_smul, orbit_submonoid_subset, mem_orbit, IsBlock.ncard_block_mul_ncard_orbit_eq, orbit_subgroup_eq_rightCoset, IsBlock.orbit, orbit_eq_iff, ConjAct.mem_orbit_conjAct, IsMinimal.dense_orbit, ConjAct.orbit_eq_carrier_conjClasses, orbit_nonempty, stabilizer_orbit_eq, SubMulAction.val_preimage_orbit, FreeGroup.Orbit.duplicate, NumberField.InfinitePlace.mem_orbit_iff, orbit_eq_univ, orbit_subgroup_one_eq_self, card_orbit_mul_card_stabilizer_eq_card_group, minimalPeriod_eq_card, subsingleton_orbit_iff_mem_fixedPoints, IsBlockSystem.of_normal, IsBlock.of_orbit, orbitRel.Quotient.orbit_eq_orbit_out, orbit_fixingSubgroup_compl_subset, mem_orbit_self, mapsTo_smul_orbit, smul_orbit_eq_orbit_smul
|
orbitRel 📖 | CompOp | 80 mathmath: MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage_of_zero, MeasureTheory.instSigmaFiniteQuotientOrbitRelOfHasFundamentalDomainOfQuotientMeasureEqMeasurePreimageVolume, WeierstrassCurve.Projective.nonsingularLift_some, isQuotientCoveringMap_quotientMk_of_properlyDiscontinuousSMul, MeasureTheory.IsFundamentalDomain.quotientMeasure_eq, WeierstrassCurve.Projective.Point.zero_point, CategoryTheory.Limits.SingleObj.Types.colimitEquivQuotient_symm_apply, WeierstrassCurve.Projective.addMap_of_Z_eq_zero_left, WeierstrassCurve.Jacobian.Point.fromAffine_some, ContinuousConstSMul.secondCountableTopology, NumberField.mixedEmbedding.fundamentalCone.integerSetQuotEquivAssociates_apply, sum_card_fixedBy_eq_card_orbits_mul_card_group, MeasureTheory.QuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient, WeierstrassCurve.Jacobian.negMap_of_Z_ne_zero, CategoryTheory.Limits.SingleObj.Types.colimitEquivQuotient_apply, card_eq_sum_card_group_div_card_stabilizer, WeierstrassCurve.Jacobian.nonsingularLift_iff, disjoint_image_image_iff, NumberField.InfinitePlace.orbitRelEquiv_apply_mk'', orbitRel_le_snd, WeierstrassCurve.Projective.smul_eq, MeasureTheory.QuotientMeasureEqMeasurePreimage.projection_respects_measure', WeierstrassCurve.Jacobian.negMap_of_Z_eq_zero, MeasureTheory.QuotientMeasureEqMeasurePreimage.isFiniteMeasure_quotient, WeierstrassCurve.Jacobian.nonsingularLift_some, isOpenMap_quotient_mk'_mul, NumberField.mixedEmbedding.fundamentalCone.quotIntNorm_apply, WeierstrassCurve.Projective.addMap_eq, image_inter_image_iff, WeierstrassCurve.Jacobian.addMap_of_Z_ne_zero, WeierstrassCurve.Jacobian.addMap_of_Z_eq_zero_right, CategoryTheory.Limits.SingleObj.colimitTypeRelEquivOrbitRelQuotient_apply, Subgroup.quotientEquivSigmaZMod_apply, WeierstrassCurve.Projective.Point.fromAffine_some, orbitRel_le_fst, WeierstrassCurve.Projective.negMap_of_Z_ne_zero, orbitRel.Quotient.subgroup_quotient_eq_iff, WeierstrassCurve.Projective.nonsingularLift_iff, orbitRel_apply, WeierstrassCurve.Jacobian.nonsingularLift_zero, isOpenQuotientMap_quotientMk, orbitRel.Quotient.orbit_mk, WeierstrassCurve.Projective.addMap_of_Y_eq, WeierstrassCurve.Projective.negMap_eq, Subgroup.transferTransversal_apply', CategoryTheory.Limits.SingleObj.colimitTypeRel_iff_orbitRel, orbitRel_subgroupOf, WeierstrassCurve.Jacobian.addMap_of_Z_eq_zero_left, WeierstrassCurve.Projective.addMap_of_Z_eq_zero_right, CategoryTheory.Limits.SingleObj.colimitTypeRelEquivOrbitRelQuotient_symm_apply, cosetToCuspOrbit_apply_mk, t2Space_quotient_mulAction_of_properSMul, WeierstrassCurve.Projective.Point.zero_def, orbitRel_subgroup_le, isConjRoot_iff_orbitRel, WeierstrassCurve.Projective.negMap_of_Z_eq_zero, WeierstrassCurve.Projective.addMap_of_Z_ne_zero, isCoveringMapOn_quotientMk_of_properlyDiscontinuousSMul, WeierstrassCurve.Jacobian.Point.zero_point, Subgroup.transferFunction_apply, automorphize_smul_left, WeierstrassCurve.Jacobian.Point.zero_def, Units.orbitRel_nonZero_iff, SubMulAction.orbitRel_of_subMul, orbitRel.Quotient.mem_orbit, Subgroup.transferTransversal_apply'', ConjAct.orbitRel_conjAct, WeierstrassCurve.Jacobian.smul_eq, MeasureTheory.IsFundamentalDomain.projection_respects_measure, WeierstrassCurve.Jacobian.addMap_eq, Subgroup.quotientEquivSigmaZMod_symm_apply, MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage_quotientMeasure, quotient_preimage_image_eq_union_mul, WeierstrassCurve.Jacobian.negMap_eq, WeierstrassCurve.Jacobian.addMap_of_Y_eq, MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quot, WeierstrassCurve.Projective.nonsingularLift_zero, MeasureTheory.IsFundamentalDomain.measurePreserving_quotient_mk, isClosedMap_quotient, t2Space_of_properlyDiscontinuousSMul_of_t2Space
|
selfEquivSigmaOrbits 📖 | CompOp | — |
selfEquivSigmaOrbits' 📖 | CompOp | — |
stabilizer 📖 | CompOp | 168 mathmath: SubMulAction.ofStabilizer.isPretransitive_iff_of_conj, SubMulAction.ofStabilizer.conjMap_comp_apply, Ideal.Quotient.map_ker_stabilizer_subtype, ConjAct.stabilizer_eq_centralizer, SubMulAction.ofStabilizer_carrier, DiscreteTiling.PlacedTile.ext_iff_of_preimage, NumberField.InfinitePlace.nat_card_stabilizer_eq_one_or_two, NumberField.InfinitePlace.isUnramified_iff_card_stabilizer_eq_one, SubMulAction.ofStabilizer.conjMap_comp_inv_apply, normalClosure_of_stabilizer_eq_top, stabilizerEquivStabilizer_symm_apply, Equiv.Perm.exists_mem_stabilizer_smul_eq, stabilizer_mul_self, DomMulAct.mem_stabilizer_iff, SubMulAction.nat_card_ofStabilizer_add_one_eq, NumberField.InfinitePlace.IsUnramified.stabilizer_eq_bot, stabilizerEquivStabilizer_trans, Equiv.Perm.exists_mem_stabilizer_isThreeCycle_of_two_lt_ncard, SubMulAction.ofStabilizer.inv_conjMap_comp_apply, NumberField.InfinitePlace.card_stabilizer, le_stabilizer_iff_smul_le, val_unitsCentralizerEquiv_apply_coe, stabilizer_inf_stabilizer_le_stabilizer_sdiff, NumberField.ComplexEmbedding.IsConj.coe_stabilizer_mk, DiscreteTiling.PlacedTile.ext_iff_of_exists, SubMulAction.ofStabilizer.isMultiplyPretransitive_iff, Ideal.Quotient.stabilizerHom_surjective, op_smul_set_stabilizer_subset, mul_stabilizer_self, index_stabilizer_of_transitive, alternatingGroup.isCoatom_stabilizer_singleton, Set.powersetCard.stabilizer_coe, IsBlock.stabilizer_le, SubMulAction.ofStabilizer.isPretransitive_iff, index_stabilizer, le_stabilizer_smul_left, SubMulAction.stabilizer_of_subMul, stabilizerEquivStabilizer_compTriple, Sylow.stabilizer_eq_normalizer, card_eq_sum_card_group_div_card_stabilizer, DiscreteTiling.PlacedTile.smul_mk_mk, stabilizer_compl, DiscreteTiling.PlacedTile.ext_iff, SubMulAction.fixingSubgroup_of_insert, Ideal.card_stabilizer_eq, DiscreteTiling.Prototile.ext_iff, alternatingGroup.stabilizer.surjective_toPerm, isCancelSMul_iff_stabilizer_eq_bot, SubMulAction.ofStabilizer.isMultiplyPretransitive_iff_of_conj, Subgroup.isComplement'_stabilizer, isCoatom_stabilizer_iff_preprimitive, card_eq_sum_card_group_div_card_stabilizer', IsBlock.orbit_stabilizer_eq, Equiv.Perm.swap_mem_stabilizer, stabilizerEquivStabilizer_apply, stabilizer_empty_eq_top, Ideal.Quotient.stabilizerHom_surjective_of_profinite, stabilizer_finset_univ, NumberField.mixedEmbedding.fundamentalCone.integerSetTorsionSMul_stabilizer, Ideal.inertia_le_stabilizer, IsPreprimitive.isCoatom_stabilizer_of_isPreprimitive, mem_stabilizer_finset, stabilizer_smul_eq_stabilizer_map_conj, SubMulAction.nat_card_ofStabilizer_eq, stabilizer_subgroup, IsFractionRing.stabilizerHom_surjective, stabilizer_finset_empty, mem_stabilizer_set_iff_subset_smul_set, DiscreteTiling.PlacedTile.coe_mk_mk, Ideal.Quotient.stabilizerHom_apply, smul_set_stabilizer_subset, Equiv.Perm.stabilizer_isPreprimitive, stabilizer_subset_div_right, isPreprimitive_fixingSubgroup_insert_iff, mem_stabilizer_set', ProperlyDiscontinuousSMul.finite_stabilizer, stabilizer_mul_eq_right, stabilizer_univ, Ideal.Quotient.stabilizerQuotientInertiaEquiv_mk, stabilizer_subgroup_op, SubMulAction.nat_card_ofStabilizer_eq_add_one, stabilizer_empty, DiscreteTiling.PlacedTile.smul_mk_coe, SubMulAction.ENat_card_ofStabilizer_add_one_eq, stabilizer_op_subgroup, CategoryTheory.PreGaloisCategory.nhds_one_has_basis_stabilizers, Module.stabilizer_units_eq_bot_of_ne_zero, NumberField.InfinitePlace.isRamified_iff_card_stabilizer_eq_two, stabilizer_finset_singleton, stabilizer_le_aestabilizer, val_unitsCentralizerEquiv_symm_apply_coe, SubMulAction.notMem_val_image, stabilizer_smul_eq_left, stabilizer_quotient, mem_stabilizer_set, mem_stabilizer_finset_iff_smul_finset_subset, Equiv.swap_mem_stabilizer, map_stabilizer_le, Topology.IsQuotientMap.isCoveringMapOn_of_smul_disjoint, orbitEquivQuotientStabilizer_symm_apply, alternatingGroup.exists_mem_stabilizer_smul_eq, SubMulAction.mem_ofStabilizer_iff, SubMulAction.ofStabilizer.snoc_castSucc, stabilizer_isOpen_of_isIntegral, Topology.IsQuotientMap.isCoveringMapOn_of_properlyDiscontinuousSMul, SubMulAction.mem_ofFixingSubgroup_insert_iff, isMultiplyPreprimitive_succ_iff_ofStabilizer, Equiv.Perm.exists_mem_stabilizer_isThreeCycle, ofQuotientStabilizer_mk, Subgroup.isComplement'_stabilizer_of_coprime, IsBlock.ncard_block_eq_relIndex, SubMulAction.ofStabilizer.conjMap_comp, mem_stabilizer_set_iff_smul_set_subset, zpowersQuotientStabilizerEquiv_symm_apply, injective_ofQuotientStabilizer, alternatingGroup.stabilizer_isPreprimitive, stabilizer_mul_eq_left, stabilizer_image_coe_quotient, SubMulAction.ofStabilizer.isMultiplyPretransitive, NumberField.InfinitePlace.not_isUnramified_iff_card_stabilizer_eq_two, Ideal.Quotient.ker_stabilizerHom, DomMulAct.stabilizerMulEquiv_apply, stabilizerEquivStabilizer_one, alternatingGroup.isCoatom_stabilizer, NumberField.InfinitePlace.isUnramified_iff_stabilizer_eq_bot, stabilizerEquivStabilizer_symm, CategoryTheory.PreGaloisCategory.stabilizer_normal_of_isGalois, Ideal.card_stabilizer_eq_card_inertia_mul_finrank, SubMulAction.ofFixingSubgroup_of_singleton_bijective, Equiv.Perm.isCoatom_stabilizer, continuousSMul_iff_stabilizer_isOpen, isCoveringMapOn_quotientMk_of_properlyDiscontinuousSMul, NumberField.InfinitePlace.mem_stabilizer_mk_iff, mem_stabilizer_iff, le_stabilizer_smul_right, stabilizer_finite, stabilizer_inf_stabilizer_le_stabilizer_inter, stabilizer_inf_stabilizer_le_stabilizer_apply₂, Finset.op_smul_stabilizer_of_no_doubling, isMultiplyPreprimitive_ofStabilizer, Equiv.Perm.stabilizer.surjective_toPerm, DiscreteTiling.PlacedTile.coe_mk_coe, stabilizer_inf_stabilizer_le_stabilizer_union, Equiv.Perm.isCoatom_stabilizer_of_ncard_lt_ncard_compl, fixingSubgroup_le_stabilizer, SubMulAction.ofStabilizer.conjMap_bijective, stabilizerEquivStabilizer_inv, Equiv.Perm.moves_in, stabilizer_isOpen, stabilizer_singleton, stabilizer_smul_eq_right, card_orbit_mul_card_stabilizer_eq_card_group, Equiv.Perm.ofSubtype_mem_stabilizer, ConjClasses.card_carrier, Ideal.instNormalSubtypeMemSubgroupStabilizerSubgroupOfInertia, SMul.smul_stabilizer_def, mem_stabilizer_finset', SubMulAction.ofStabilizer.conjMap_apply, ofQuotientStabilizer_smul, stabilizer_coe_finset, Subgroup.nat_card_centralizer_nat_card_stabilizer, SubMulAction.ofFixingSubgroup_insert_map_bijective, IsCancelSMul.stabilizer_eq_bot, Finset.smul_stabilizer_of_no_doubling, mem_stabilizer_finset_iff_subset_smul_finset, Subgroup.centralizer_eq_comap_stabilizer, alternatingGroup.isCoatom_stabilizer_of_ncard_lt_ncard_compl, stabilizer_univ_eq_top
|
stabilizerSubmonoid 📖 | CompOp | 4 mathmath: SubMulAction.stabilizer_of_subMul.submonoid, mem_stabilizerSubmonoid_iff, CategoryTheory.ActionCategory.stabilizerIsoEnd_apply, CategoryTheory.ActionCategory.stabilizerIsoEnd_symm_apply
|