Aut

📁 Source: Mathlib/Data/ZMod/Aut.lean

Statistics

Metric	Count
Definitions Aut, Aut, AddAutEquivUnits	3
Theorems AddAutEquivUnits_apply, AddAutEquivUnits_symm_apply	2
Total	5

CategoryTheory

Definitions

Name	Category	Theorems
Aut 📖	CompOp	103 math math: PreGaloisCategory.instT2SpaceAutFunctorFintypeCat, PreGaloisCategory.mulAction_def, Iso.conjAut_apply, PreGaloisCategory.instFiniteAutOfIsConnected, PreGaloisCategory.autEmbedding_injective, PreGaloisCategory.instContinuousMulAutFunctorFintypeCat, PreGaloisCategory.autMap_comp, PreGaloisCategory.toAutMulEquiv_isHomeomorph, Aut.Aut_mul_def, PreGaloisCategory.instEssSurjContActionFintypeCatHomCarrierAutFunctorFunctorToContAction, PreGaloisCategory.card_aut_le_card_fiber_of_connected, Functor.FullyFaithful.autMulEquivOfFullyFaithful_symm_apply_hom, PreGaloisCategory.isGalois_iff_aux, PreGaloisCategory.instTotallyDisconnectedSpaceAutFunctorFintypeCat, Iso.conjAut_mul, PreGaloisCategory.autMapHom_apply, Aut.toEnd_apply, PreGaloisCategory.toAut_hom_app_apply, PreGaloisCategory.instFaithfulActionFintypeCatAutFunctorFunctorToAction, Functor.FullyFaithful.autMulEquivOfFullyFaithful_apply_inv, Functor.FullyFaithful.autMulEquivOfFullyFaithful_apply_hom, PreGaloisCategory.instFullContActionFintypeCatHomCarrierAutFunctorFunctorToContAction, Iso.trans_conjAut, PreGaloisCategory.autIsoFibers_inv_app, PreGaloisCategory.functorToContAction_map, PreGaloisCategory.continuous_mapAut_whiskeringRight, PreGaloisCategory.instPreservesIsConnectedActionFintypeCatAutFunctorFunctorToAction, Functor.map_conjAut, Aut.Aut_inv_def, PreGaloisCategory.toAutHomeo_apply, PreGaloisCategory.instIsEquivalenceContActionFintypeCatHomCarrierAutFunctorFunctorToContAction, PreGaloisCategory.exists_lift_of_continuous, PreGaloisCategory.toAutMulEquiv_apply, PreGaloisCategory.toAut_isHomeomorph, PreGaloisCategory.exists_lift_of_mono_of_isConnected, PreGaloisCategory.evaluation_aut_bijective_of_isGalois, PreGaloisCategory.instIsFundamentalGroupAutFunctorFintypeCat, PreGaloisCategory.instPreservesColimitsOfShapeActionFintypeCatAutFunctorSingleObjFunctorToActionOfFinite, PreGaloisCategory.toAut_surjective_of_isPretransitive, PreGaloisCategory.autMulEquivAutGalois_symm_app, PreGaloisCategory.continuousSMul_aut_fiber, PreGaloisCategory.exists_autMap, Units.toAut_hom, PreGaloisCategory.FiberFunctor.isPretransitive_of_isConnected, PreGaloisCategory.evaluationEquivOfIsGalois_apply, PreGaloisCategory.aut_discreteTopology, PreGaloisCategory.nhds_one_has_basis_stabilizers, PreGaloisCategory.autMap_surjective_of_isGalois, PreGaloisCategory.functorToAction_map, PreGaloisCategory.autMap_apply_mul, Action.ρAut_apply_hom, Functor.FullyFaithful.autMulEquivOfFullyFaithful_symm_apply_inv, PreGaloisCategory.instPreservesFiniteCoproductsActionFintypeCatAutFunctorFunctorToAction, PreGaloisCategory.autMulEquivAutGalois_π, PreGaloisCategory.isGalois_iff_pretransitive, PreGaloisCategory.instPreservesMonomorphismsActionFintypeCatAutFunctorFunctorToAction, PreGaloisCategory.instFaithfulContActionFintypeCatHomCarrierAutFunctorFunctorToContAction, PreGaloisCategory.autEmbedding_apply, PreGaloisCategory.stabilizer_normal_of_isGalois, PreGaloisCategory.instEssSurjContActionFintypeCatHomCarrierAutFunctorFunctorToContActionOfFiberFunctor, PreGaloisCategory.instReflectsIsomorphismsActionFintypeCatAutFunctorFunctorToAction, PreGaloisCategory.evaluation_aut_surjective_of_isGalois, Units.toAut_inv, Iso.conjAut_hom, PreGaloisCategory.evaluationEquivOfIsGalois_symm_fiber, PreGaloisCategory.autEmbedding_range, PreGaloisCategory.IsGalois.quotientByAutTerminal, PreGaloisCategory.mulAction_naturality, PreGaloisCategory.AutGalois.π_apply, PreGaloisCategory.exists_lift_of_mono, Iso.conjAut_zpow, PreGaloisCategory.functorToContAction_obj_obj, PreGaloisCategory.FiberFunctor.isPretransitive_of_isGalois, PreGaloisCategory.endEquivAutGalois_π, PreGaloisCategory.instIsTopologicalGroupAutFunctorFintypeCat, PreGaloisCategory.exists_lift_of_quotient_openSubgroup, PreGaloisCategory.autGaloisSystem_map, PreGaloisCategory.toAut_bijective, PreGaloisCategory.isPretransitive_of_isGalois, PreGaloisCategory.AutGalois.π_surjective, PreGaloisCategory.instCompactSpaceAutFunctorFintypeCat, PreGaloisCategory.instReflectsMonomorphismsActionFintypeCatAutFunctorFunctorToAction, Action.ρAut_apply_inv, Iso.conjAut_pow, TannakaDuality.FiniteGroup.equivHom_surjective, PreGaloisCategory.toAut_injective_of_non_trivial, TannakaDuality.FiniteGroup.equivHom_injective, PreGaloisCategory.endMulEquivAutGalois_pi, FintypeCat.instFiniteAut, PreGaloisCategory.instIsPretransitiveAutCarrierVFintypeCatFunctorObjActionFunctorToActionOfIsGalois, PreGaloisCategory.evaluation_aut_injective_of_isConnected, PreGaloisCategory.instContinuousSMulAutFintypeCatObjCarrier, PreGaloisCategory.functorToAction_full, TannakaDuality.FiniteGroup.equivHom_apply, PreGaloisCategory.autGaloisSystem_obj_coe, PreGaloisCategory.toAut_continuous, PreGaloisCategory.autEmbedding_isClosedEmbedding, PreGaloisCategory.instContinuousInvAutFunctorFintypeCat, PreGaloisCategory.autMap_id, Iso.conjAut_trans, PreGaloisCategory.instPreservesFiniteProductsActionFintypeCatAutFunctorFunctorToAction, PreGaloisCategory.autEmbedding_range_isClosed, PreGaloisCategory.functorToAction_comp_forget₂_eq

RootPairing

Definitions

Name	Category	Theorems
Aut 📖	CompOp	27 math math: weylGroup_toSubmonoid, span_orbit_eq_top, range_weylGroup_coweightHom, Equiv.weightHom_toLinearMap, Equiv.toEndUnit_inv, weylGroup_apply_root, Equiv.root_indexEquiv_eq_smul, Equiv.coweightHom_injective, isSimpleModule_weylGroupRootRep, InvariantForm.apply_weylGroup_smul, isSimpleModule_weylGroupRootRep_iff, Equiv.weightHom_apply, reflection_mem_weylGroup, range_weylGroupToPerm, Equiv.indexHom_apply, Equiv.instSMulCommClassAut, weylGroup.ofIdx_smul, Equiv.coweightHom_op, Equiv.reflection_inv, Equiv.weightHom_injective, Equiv.reflection_smul, range_weylGroup_weightHom, Equiv.coweightHom_toLinearMap, Equiv.instSMulCommClassMulOppositeAut, Equiv.coweightHom_apply, Equiv.indexEquiv_inv, Equiv.toEndUnit_val

ZMod

Definitions

Name	Category	Theorems
AddAutEquivUnits 📖	CompOp	2 math math: AddAutEquivUnits_symm_apply, AddAutEquivUnits_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
AddAutEquivUnits_apply 📖	mathematical	—	DFunLike.coe MulEquiv AddAut ZMod Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AddAut.instGroup Units.instMul EquivLike.toFunLike MulEquiv.instEquivLike AddAutEquivUnits Units.mkOfMulEqOne AddEquiv AddEquiv.instEquivLike AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
AddAutEquivUnits_symm_apply 📖	mathematical	—	DFunLike.coe MulEquiv Units ZMod MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring commRing AddAut Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Units.instMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid AddAut.instGroup EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm AddAutEquivUnits MonoidHom NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Units.instMulOneClass MonoidHom.instFunLike AddAut.mulLeft	—	—

---

← Back to Index