Defs

📁 Source: Mathlib/Algebra/Group/Equiv/Defs.lean

Statistics

Metric	Count
Definitions AddEquiv, symm_apply, cast, instCoeFunForall, instEquivLike, instInhabited, mk', ofBijective, refl, symmEquiv, toAddHom, toAddMonoidHom, toEquiv, trans, AddEquivClass, toAddEquiv, toAddEquiv, toAddEquiv, toMulEquiv, MulEquiv, symm_apply, cast, instCoeFunForall, instEquivLike, instInhabited, mk', ofBijective, refl, symmEquiv, toEquiv, toMonoidHom, toMulHom, trans, MulEquivClass, toMulEquiv, toMulEquiv, instCoeTCAddEquivOfAddEquivClass, instCoeTCMulEquivOfMulEquivClass, «term_≃*_», «term_≃+_»	40
Theorems apply_eq_iff_eq, apply_eq_iff_symm_apply, apply_symm_apply, bijective, cast_apply, cast_symm_apply, coe_addMonoidHom_comp_coe_addMonoidHom_symm, coe_addMonoidHom_refl, coe_addMonoidHom_symm_comp_coe_addMonoidHom, coe_addMonoidHom_trans, coe_mk, coe_refl, coe_toAddHom, coe_toAddMonoidHom, coe_toEquiv, coe_toEquiv_symm, coe_trans, comp_left_injective, comp_right_injective, comp_symm_eq, congr_arg, congr_fun, eq_comp_symm, eq_symm_apply, eq_symm_comp, equivLike_neg_eq_symm, ext, ext_iff, injective, instAddEquivClass, invFun_eq_symm, map_add, map_add', map_eq_zero_iff, map_ne_zero_iff, map_neg, map_sub, map_zero, mk_coe, mk_coe', ofBijective_apply, ofBijective_apply_symm_apply, refl_apply, refl_symm, self_comp_symm, self_trans_symm, surjective, symmEquiv_apply_apply, symmEquiv_apply_symm_apply, symmEquiv_symm_apply_apply, symmEquiv_symm_apply_symm_apply, symm_apply_apply, symm_apply_eq, symm_bijective, symm_comp_eq, symm_comp_self, symm_map_add, symm_mk, symm_symm, symm_trans_apply, symm_trans_self, toAddHom_eq_coe, toAddMonoidHom_eq_coe, toAddMonoidHom_injective, toEquiv_eq_coe, toEquiv_injective, toEquiv_symm, toFun_eq_coe, trans_apply, apply_coe_symm_apply, coe_symm_apply_apply, instAddHomClass, instAddMonoidHomClass, map_add, map_eq_zero_iff, map_ne_zero_iff, toAddEquiv_apply, toAddEquiv_symm_apply, toAddEquiv_apply, toAddEquiv_symm_apply, map_eq_one_iff, map_eq_zero_iff, map_ne_one_iff, map_ne_zero_iff, toMulEquiv_apply, toMulEquiv_symm_apply, apply_eq_iff_eq, apply_eq_iff_symm_apply, apply_symm_apply, bijective, cast_apply, cast_symm_apply, coe_mk, coe_monoidHom_comp_coe_monoidHom_symm, coe_monoidHom_refl, coe_monoidHom_symm_comp_coe_monoidHom, coe_monoidHom_trans, coe_refl, coe_toEquiv, coe_toEquiv_symm, coe_toMonoidHom, coe_toMulHom, coe_trans, comp_left_injective, comp_right_injective, comp_symm_eq, congr_arg, congr_fun, eq_comp_symm, eq_symm_apply, eq_symm_comp, equivLike_inv_eq_symm, ext, ext_iff, injective, instMulEquivClass, invFun_eq_symm, map_div, map_eq_one_iff, map_inv, map_mul, map_mul', map_ne_one_iff, map_one, mk_coe, mk_coe', ofBijective_apply, ofBijective_apply_symm_apply, refl_apply, refl_symm, self_comp_symm, self_trans_symm, surjective, symmEquiv_apply_apply, symmEquiv_apply_symm_apply, symmEquiv_symm_apply_apply, symmEquiv_symm_apply_symm_apply, symm_apply_apply, symm_apply_eq, symm_bijective, symm_comp_eq, symm_comp_self, symm_map_mul, symm_mk, symm_symm, symm_trans_apply, symm_trans_self, toEquiv_eq_coe, toEquiv_injective, toEquiv_symm, toFun_eq_coe, toMonoidHom_eq_coe, toMonoidHom_injective, toMulHom_eq_coe, trans_apply, apply_coe_symm_apply, coe_symm_apply_apply, instMonoidHomClass, instMulHomClass, map_eq_one_iff, map_mul, map_ne_one_iff, toMulEquiv_apply, toMulEquiv_symm_apply	164
Total	204

AddEquiv

Definitions

Name	Category	Theorems
cast 📖	CompOp	2 math math: cast_apply, cast_symm_apply
instCoeFunForall 📖	CompOp	—
instEquivLike 📖	CompOp	646 math math: val_toAddUnits_apply, AddSubgroup.centerToAddOpposite_apply_coe, DFinsupp.liftAddHom_apply, CochainComplex.HomComplex.Cochain.rightShiftAddEquiv_symm_apply, coprodComm_apply, AddMonoidAlgebra.mapDomainRingEquiv_apply, ofLeftInverse'_apply, ContinuousMap.addEquivBoundedOfCompact_apply, AddMonoidAlgebra.domCongr_comp_lsingle, AddSubmonoid.LocalizationMap.symm_comp_ofAddEquivOfLocalizations_apply, WithConv.addEquiv_symm_apply_ofConv, AddSubmonoid.LocalizationMap.addEquivOfAddEquiv_eq, CochainComplex.HomComplex.Cocycle.leftShiftAddEquiv_symm_apply, MonomialOrder.degree_add_of_ne, Multiset.toFinsupp_add, AddAut.apply_inv_self, Rep.diagonalSuccIsoFree_inv_hom_single, CochainComplex.HomComplex.Cocycle.equivHom_symm_apply, addSubgroupMap_symm_apply, piAdditive_apply, Multiset.equivDFinsupp_symm_apply, DFinsupp.liftAddHom_apply_single, WithLp.addEquiv_apply, toAddMonoidHom_eq_coe, AddAutAdditive_apply_symm_apply, Complex.equivRealProdAddHom_symm_apply, Rep.leftRegularHom_hom, AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid_apply_coe, AddMonoidHom.ker_comp_addEquiv, invFun_eq_symm, AddSubgroup.index_map_equiv, AddMonoidHom.toAddEquiv_symm_apply, Subring.addEquivOp_apply_coe, prodUnique_apply, CochainComplex.HomComplex.Cochain.fromSingleEquiv_fromSingleMk, WithConv.toEquiv_addEquiv, Matrix.entryAddHom_eq_comp, AddSubgroup.addSubgroupOfContinuousAddEquivOfLe_apply, Finsupp.sumFinsuppAddEquivProdFinsupp_symm_inl, AddMonoidAlgebra.mapRangeAddEquiv_apply, coprodPUnit_symm_apply, HahnSeries.addOppositeEquiv_symm_support, AddAut.mulRight_symm_apply, MulEquiv.toAdditive_apply_apply, AddMonoidAlgebra.mapDomainAddEquiv_single, CategoryTheory.Abelian.Ext.mk₀_addEquiv₀_apply, SubAddAction.ofStabilizer.conjMap_comp, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_left, AddAut.mul_apply, additiveMultiplicative_apply, sigmaFinsuppAddEquivDFinsupp_apply, AddSubmonoid.fromLeftNeg_leftNegEquiv_symm, neg_apply, MulOpposite.opAddEquiv_apply, AddSubgroup.comap_equiv_eq_map_symm, AddMonoidAlgebra.domCongr_toAlgHom, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_postcomp, AddSubmonoid.val_neg_addUnitsTypeEquivIsAddUnitAddSubmonoid_symm_apply, AddMonoidAlgebra.mapDomainAddEquiv_apply, MultilinearMap.domDomCongrEquiv_symm_apply, AddSubmonoid.LocalizationMap.addEquivOfLocalizations_symm_apply, MonomialOrder.degree_sub_le, Finsupp.sigmaFinsuppAddEquivPiFinsupp_apply, AddEquivClass.apply_coe_symm_apply, AddSubmonoid.add_leftNegEquiv_symm, map_zero, multiplesAddHom_apply, val_neg_piAddUnits_apply, uliftMultiplesHom_symm_apply, funUnique_symm_apply, AddHom.toAddEquiv_apply, coe_prodComm_symm, symm_comp_eq, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_right, AddHom.toAddEquiv_symm_apply, AddSubmonoid.coe_equivMapOfInjective_apply, AddMonoidAlgebra.toRingHom_mapDomainRingEquiv, addSubgroupCongr_apply, Set.conj_mem_fixingAddSubgroup, piUnique_apply, Matrix.uniqueAddEquiv_apply, RingEquiv.op_apply_symm_apply, AddAutAdditive_apply_apply, AddSubmonoid.LocalizationMap.addEquivOfAddEquiv_mk', Finsupp.toMultiset_toFinsupp, AddEquivClass.coe_symm_apply_apply, Finsupp.mapRange.addEquiv_apply, AddAutAdditive_symm_apply_symm_apply, MonomialOrder.degree_reduce_lt, AddOpposite.opAddEquiv_apply, Finsupp.llift_apply, QuotientAddGroup.liftEquiv_coe, AddSubmonoid.LocalizationMap.ofAddEquivOfLocalizations_eq_iff_eq, AddSubsemigroup.mem_map_equiv, comp_symm_eq, Multiset.toFinsupp_sum_eq, AddMonoidHom.apply_ofInjective_symm, Finsupp.sumFinsuppAddEquivProdFinsupp_symm_apply, AddUnits.coe_unop_opEquiv, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, MulAutMultiplicative_symm_apply_apply, AddSubgroup.mem_iff_toAddUnits_mem_addUnits, sigmaFinsuppAddEquivDFinsupp_symm_apply, AddMagmaCat.addEquiv_coe_eq, zmultiplesAddHom_symm_apply, finsuppUnique_symm, coe_addMonoidHom_refl, Representation.smul_ofModule_asModule, MonomialOrder.toSyn_strictMono, CochainComplex.HomComplex.Cocycle.equivHomShift'_symm_apply, WeierstrassCurve.Projective.Point.toAffineAddEquiv_apply, MonomialOrder.div_single, Subsemiring.addEquivOp_apply_coe, Finsupp.liftAddHom_comp_single, MonoidAlgebra.mapDomainAddEquiv_single, multiplesAddHom_symm_apply, AddSubmonoid.centerCongr_symm_apply_coe, SubAddAction.ofStabilizer.conjMap_comp_neg_apply, AddSubgroup.coe_equivMapOfInjective_apply, symmEquiv_symm_apply_symm_apply, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, MulAutMultiplicative_apply_apply, Finsupp.mapRange.addEquiv_toEquiv, withZeroCongr_apply, Matrix.coe_ofAddEquiv_symm, MonomialOrder.degree_add_le, AddSubsemigroup.topEquiv_apply, prodProdProdComm_apply, coe_addMonoidHom_comp_coe_addMonoidHom_symm, Multiset.equivDFinsupp_apply, self_comp_symm, CochainComplex.HomComplex.CohomologyClass.toSmallShiftedHom_mk, addEquivOfAddOrderOfEq_apply_gen, Matrix.uniqueAddEquiv_symm_apply, HahnSeries.addOppositeEquiv_support, AddSubmonoid.centerToAddOpposite_symm_apply_coe, AddMonoidHom.ofLeftInverse_symm_apply, Subalgebra.mopAlgEquivOp_symm_apply, AddSubsemigroup.centerToAddOpposite_symm_apply_coe, DFinsupp.mapRange.addEquiv_apply, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_symm_apply, AddSemigrp.addEquiv_coe_eq, AddAut.conj_symm_apply, Matrix.entryAddMonoidHom_eq_comp, uniqueProd_symm_apply, MonomialOrder.le_degree, SubAddAction.conjMap_ofFixingAddSubgroup_bijective, CategoryTheory.Adjunction.compPreadditiveYonedaIso_inv_app_app_apply, AddSubsemigroup.comap_equiv_eq_map_symm, map_dfinsuppSumAddHom, FreeAbelianGroup.liftAddEquiv_symm_apply, AddSubmonoid.LocalizationMap.of_addEquivOfAddEquiv_apply, addMonoidHomCongrLeft_apply, LinearEquiv.funUnique_symm_apply, AddSubmonoid.LocalizationMap.symm_comp_ofAddEquivOfLocalizations_apply', AddSubgroup.mem_ofAddUnits_iff_toAddUnits_mem, symm_apply_apply, QuotientAddGroup.liftEquiv_mk, AddSubgroup.addSubgroupOfEquivOfLe_apply_coe, AddAut.coe_inv, SubAddAction.conjMap_ofFixingAddSubgroup_coe_apply, Multiset.toFinsupp_union, toAdditive_toMultiplicative_symm_apply, AlgEquiv.op_apply_symm_apply, AddSubmonoid.leftNegEquiv_add, Unitization.cobounded_eq_aux, DirectSum.addEquivProdDirectSum_symm_apply_toFun, CategoryTheory.Iso.addCommGroupIsoToAddEquiv_symm_apply, map_eq_zero_iff, coe_addEquiv_lpPiLp_symm, MonomialOrder.lex_lt_iff_of_unique, SkewMonoidAlgebra.toFinsuppAddEquiv_apply, MulAutMultiplicative_symm_apply_symm_apply, FreeAbelianGroup.equivFinsupp_symm_apply, ModuleCat.homAddEquiv_symm_apply_hom, AddSubmonoid.map_equiv_top, MonomialOrder.degLex_le_iff, coe_prodAssoc, coprodAssoc_apply_inr, AddSubmonoid.LocalizationMap.addEquivOfAddEquiv_eq_map_apply, Finsupp.comp_liftAddHom, piUnique_symm_apply, funUnique_apply, SubAddAction.ofFixingAddSubgroup_of_eq_bijective, coe_addSubmonoidMap_apply, comp_left_injective, AddCommGrpCat.homAddEquiv_symm_apply_hom, ofLeftInverse_apply, Multiset.toFinsupp_inter, MonomialOrder.degree_le_iff, AddMonoidAlgebra.domCongr_single, CategoryTheory.ProjectiveResolution.extMk_hom, AddSubsemigroup.topEquiv_symm_apply_coe, op_symm_apply_symm_apply, Finsupp.domCongr_apply, Rep.toAdditive_symm_apply, AddAut.coe_mul, AddSubgroup.centerCongr_apply_coe, OrderAddMonoidIso.coe_addEquiv, Finsupp.lift_apply, AddSubmonoid.comap_equiv_eq_map_symm, subsemigroupMap_apply_coe, CochainComplex.HomComplex.Cochain.leftShiftAddEquiv_apply, Multiset.toFinsupp_apply, neg'_apply, AddCircle.equivAddCircle_apply_mk, CochainComplex.HomComplex.Cochain.rightShiftAddEquiv_apply, OrderAddMonoidIso.coe_mk, finsuppUnique_apply, AddSubsemigroup.centerCongr_apply_coe, AddAction.zmultiplesQuotientStabilizerEquiv_symm_apply, AddSubgroup.map_equiv_eq_comap_symm, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, Finset.mapRange_finsuppAntidiag_eq, Rep.indResAdjunction_counit_app_hom_hom, QuaternionAlgebra.coe_addEquivProd, RingEquiv.coe_toAddEquiv, AddAction.stabilizerEquivStabilizer_symm_apply, AddCon.comap_conGen_equiv, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_pow', toEquiv_symm, prodProdProdComm_toEquiv, QuadraticForm.dualProdIsometry_invFun, entryAddHom_comp_mapMatrix, MonomialOrder.degree_sum_le, AddCon.comapQuotientEquivOfSurj_symm_mk, AddLocalization.addEquivOfQuotient_mk', symmEquiv_apply_symm_apply, Subring.mopRingEquivOp_symm_apply, map_finsum_mem, AddMonoid.IsTorsion.torsionAddEquiv_symm_apply_coe, add_submonoid_map_symm_apply, AddSubmonoid.map_coe_toAddEquiv, AddSubmonoid.val_addUnitsTypeEquivIsAddUnitAddSubmonoid_symm_apply, Finsupp.snd_sumFinsuppAddEquivProdFinsupp, mapAddSubgroup_symm_apply, Complex.equivRealProdAddHom_symm_apply_re, arrowCongr_apply, Equiv.addEquiv_apply, coprodPUnit_apply, AddMonoidHom.ofLeftInverse_apply, Complex.equivRealProdAddHom_symm_apply_im, Subsemiring.addEquivOp_symm_apply_coe, MonomialOrder.degree_mul_lt_iff_left_lt_of_ne_zero, Finsupp.coe_curryAddEquiv, AddSubmonoid.LocalizationMap.ofAddEquivOfDom_apply, MonomialOrder.degree_smul_le, bijective, FreeAddMonoid.freeAddMonoidCongr_of, AddSubmonoid.add_leftNegEquiv, SubAddAction.ofFixingAddSubgroup_insert_map_bijective, AddAut.conj_inv_apply, ZMod.AddAutEquivUnits_apply, comp_right_injective, toMultiplicativeLeft_symm_apply_symm_apply, MonoidAlgebra.mapRangeAddEquiv_apply, coprodAssoc_symm_apply_inr_inr, mapMatrix_apply, groupCohomology.norm_ofAlgebraAutOnUnits_eq, MonomialOrder.degree_mul_le, AddSubmonoid.leftNegEquiv_symm_add, CategoryTheory.InducedCategory.homAddEquiv_symm_apply_hom, coe_refl, Rep.toAdditive_apply, eq_comp_symm, CochainComplex.HomComplex.CohomologyClass.equiv_toSmallShiftedHom_mk, SemimoduleCat.homAddEquiv_apply, DirectSum.addEquivProdDirectSum_apply, comapAddSubgroup_apply, MonomialOrder.le_add_right, toMultiplicativeRight_symm_apply_apply, AddSubmonoid.LocalizationMap.ofAddEquivOfLocalizations_apply, coe_trans, AddSubgroup.addSubgroupOfEquivOfLe_symm_apply_coe_coe, MonomialOrder.degree_pow_le, piAdditive_symm_apply, AddSubsemigroup.strictMono_topEquiv, AddSubmonoid.leftNegEquiv_symm_fromLeftNeg, DirectSum.addEquivProdDirectSum_symm_apply_support', AddSubmonoid.leftNegEquiv_apply, AddSubgroup.comap_toAddSubmonoid, groupHomology.H1AddEquivOfIsTrivial_single, Relation.cutExpand_le_invImage_lex, Finsupp.liftAddHom_apply, MonomialOrder.toSyn_monotone, AddSubsemigroup.map_equiv_eq_comap_symm, SubAddAction.ofFixingAddSubgroup_of_eq_apply, starL_symm_apply, coprodAssoc_apply_inl_inr, coprodCongr_apply, WeierstrassCurve.Jacobian.Point.toAffineAddEquiv_apply, MonomialOrder.degLex_single_le_iff, AddSubgroup.topEquiv_symm_apply_coe, CategoryTheory.Abelian.Ext.homAddEquiv_apply, SkewMonoidAlgebra.toFinsuppAddEquiv_symm_apply, apply_symm_apply, AddLocalization.addEquivOfQuotient_apply, QuotientAddGroup.quotientAddEquivOfEq_mk, uliftMultiplesHom_apply_apply, Finsupp.sumFinsuppAddEquivProdFinsupp_apply, Finset.mapRange_finsuppAntidiag_subset, equivLike_neg_eq_symm, strictMono_subsemigroupCongr, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_apply, FreeAddGroup.freeAddGroupCongr_apply, prodAdditive_apply, AddMonoidHom.toAddEquiv_apply, AlgEquiv.op_symm_apply_symm_apply, AddSubsemigroup.map_equiv_top, coe_addSubgroupMap_apply, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_pow, Multiset.toFinsupp_singleton, Matrix.conjTransposeAddEquiv_apply, AlternatingMap.domDomCongrEquiv_apply, AddGroupExtension.Equiv.rightHom_comm, AddSubsemigroup.coe_equivMapOfInjective_apply, Multiset.toFinsupp_symm_apply, FreeAbelianGroup.equivFinsupp_apply, CategoryTheory.Abelian.Ext.biprodAddEquiv_apply_fst, ofBijective_apply, cast_apply, AddSubmonoid.topEquiv_symm_apply_coe, AddLocalization.addEquivOfQuotient_mk, Representation.ofModule_asModule_act, CategoryTheory.InducedCategory.homAddEquiv_apply, CategoryTheory.Adjunction.compPreadditiveYonedaIso_hom_app_app_apply, congr_arg, Matrix.piAddEquiv_symm_apply, QuadraticForm.dualProdIsometry_toFun, QuotientAddGroup.quotientKerEquivOfRightInverse_symm_apply, HahnSeries.addOppositeEquiv_orderTop, coprodAssoc_symm_apply_inl, AddOpposite.coe_opAddEquiv, punitCoprod_symm_apply, symmEquiv_symm_apply_apply, starL'_symm_apply, AddSubgroup.centerCongr_symm_apply_coe, prodAdditive_symm_apply, CochainComplex.HomComplex.Cocycle.rightShiftAddEquiv_symm_apply, FreeAddMonoid.freeAddMonoidCongr_symm_of, coe_prodComm, coe_toEquiv_symm, surjective, coe_prodAssoc_symm, AddLocalization.addEquivOfQuotient_symm_mk', addDissociated_preimage, AddAut.coe_one, RestrictScalars.lsmul_apply_apply, coe_addMonoidHom_trans, groupHomology.H1AddEquivOfIsTrivial_symm_apply, toMultiplicativeRight_symm_apply_symm_apply, AddAut.mulRight_apply, AddChar.coe_doubleDualEquiv, Finsupp.coe_orderIsoMultiset_symm, SubAddAction.ofStabilizer.conjMap_bijective, addOrderOf_eq, Finsupp.fst_sumFinsuppAddEquivProdFinsupp, Matrix.transposeAddEquiv_apply, coe_addEquiv_lpBCF_symm, toMultiplicative_symm_apply_apply, DistribMulAction.toAddEquiv_apply, addEquivOfAddOrderOfEq_symm_apply_gen, SubAddAction.ofFixingAddSubgroup_insert_map_apply, Subalgebra.algEquivOpMop_apply, toAddHom_eq_coe, addSubmonoidMap_symm_apply, AddSubmonoid.topEquiv_apply, Complex.equivRealProdAddHom_apply, AddSubmonoid.equivMapOfInjective_coe_addEquiv, MonomialOrder.toSyn_eq_zero_iff, AddAut.conj_apply, AddOpposite.coe_symm_opAddEquiv, QuotientAddGroup.quotientBot_apply, AddSubsemigroup.centerCongr_symm_apply_coe, symm_trans_apply, mapAddSubgroup_apply, AlgEquiv.subalgebraMap_apply_coe, coe_ofLexAddEquiv, QuotientAddGroup.quotientKerEquivOfRightInverse_apply, symm_comp_self, uliftZMultiplesHom_apply_apply, Multiset.toFinsupp_zero, CochainComplex.HomComplex.Cocycle.equivHomShift'_apply, opOp_symm_apply, Multiset.toFinsupp_toMultiset, MonomialOrder.degree_prod_le, RestrictScalars.addEquiv_symm_map_smul_smul, RingEquiv.op_symm_apply_symm_apply, WithConv.addEquiv_apply, RingEquiv.nonUnitalSubsemiringMap_symm_apply_coe, AddSubgroup.mem_map_equiv, MonomialOrder.div_set, AddMonoidAlgebra.mapDomainRingEquiv_single, CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv_symm_apply, HahnSeries.addOppositeEquiv_symm_orderTop, DFinsupp.comp_liftAddHom, symm_apply_eq, map_add, ext_iff, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_apply, AddMonoidAlgebra.domCongr_support, coe_addEquiv_lpBCF, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_zpow', MonomialOrder.degLex_lt_iff, Finsupp.mapRange.addEquiv_toAddMonoidHom, QuaternionAlgebra.coe_symm_addEquivProd, MulOpposite.opAddEquiv_toEquiv, Nat.factorization_eq_primeFactorsList_multiset, opOp_apply, AddSubmonoid.LocalizationMap.addEquivOfLocalizations_left_neg_apply, CategoryTheory.InjectiveResolution.extMk_hom, AddAut.inv_apply, ofLeftInverse'_symm_apply, SubAddAction.fixingAddSubgroupEquivFixingAddSubgroup_coe_apply, groupHomology.H1AddEquivOfIsTrivial_apply, AddSubgroup.centerToAddOpposite_symm_apply_coe, AddSubmonoid.centerCongr_apply_coe, injective, AddOpposite.opAddEquiv_symm_apply, Rep.unit_iso_comm, toMultiplicative_symm_apply_symm_apply, CategoryTheory.Adjunction.homAddEquiv_symm_apply, apply_eq_iff_eq, congr_fun, Multiset.toFinsupp_eq_iff, val_piAddUnits_symm_apply, cast_symm_apply, AddMonoid.IsTorsion.torsionAddEquiv_apply, additiveMultiplicative_symm_apply, AddLocalization.addEquivOfQuotient_symm_mk, DistribMulAction.toAddEquiv_symm_apply, Unitization.isUniformEmbedding_addEquiv, DirectSum.equivCongrLeft_apply, coe_symm_toNatLinearEquiv, Finsupp.liftAddHom_singleAddHom, finsuppUnique_symm_apply_support_val, HahnSeries.addOppositeEquiv_symm_leadingCoeff, CategoryTheory.Abelian.Ext.addEquiv₀_symm_apply, HahnSeries.addOppositeEquiv_leadingCoeff, Finsupp.domLCongr_apply, AddSubgroup.topEquiv_apply, instAddEquivClass, AddAction.stabilizerEquivStabilizer_apply, toEquiv_eq_coe, DFinsupp.liftAddHom_singleAddHom, Representation.ofModule_asAlgebraHom_apply_apply, QuotientAddGroup.quotientBot_symm_apply, Finsupp.lift_symm_apply, AddSubmonoid.LocalizationMap.ofAddEquivOfDom_comp_symm, coe_addEquiv_lpPiLp, toAdditive_toMultiplicative_apply, coe_toIntLinearEquiv, addSubgroupCongr_symm_apply, AddLocalization.addEquivOfQuotient_addMonoidOf, MulEquiv.toAdditive_apply_symm_apply, AddAut.mulLeft_apply_apply, coe_toEquiv, AddSubgroup.equivMapOfInjective_coe_addEquiv, CochainComplex.HomComplex.Cocycle.equivHomShift_comp, ext_int_iff, coe_addMonoidHom_symm_comp_coe_addMonoidHom, Finsupp.liftAddHom_apply_single, AddLocalization.addEquivOfQuotient_symm_addMonoidOf, SubAddAction.ofStabilizer.neg_conjMap_comp_apply, ContinuousAddEquiv.coe_mk, AddGroupExtension.Equiv.coe_toAddEquiv, CochainComplex.HomComplex.Cocycle.equivHom_apply, AlgEquiv.opComm_symm_apply_symm_apply, symmEquiv_apply_apply, DirectSum.decomposeAddEquiv_symm_apply, MonoidAlgebra.mapRangeAddEquiv_single, MulAutMultiplicative_apply_symm_apply, AddChar.doubleDualEquiv_symm_doubleDualEmb_apply, WithLp.coe_addEquiv, subsemigroupMap_symm_apply_coe, MonomialOrder.lex_lt_iff, refl_apply, DirectSum.decomposeAddEquiv_apply, AddSubmonoid.LocalizationMap.ofAddEquivOfDom_comp, AddMonoidAlgebra.mapRangeAddEquiv_single, finsuppAddEquivDFinsupp_apply, ContinuousMap.addEquivBoundedOfCompact_symm_apply, AddMonoidAlgebra.domCongr_apply, coe_toNatLinearEquiv, AddSubgroup.map_symm_eq_iff_map_eq, finsuppAddEquivDFinsupp_symm_apply, AddAut.one_apply, trans_apply, AddSubsemigroup.topEquiv_toAddHom, AddGroupExtension.Equiv.inl_comm, Finsupp.liftAddHom_symm_apply_apply, toMultiplicativeLeft_symm_apply_apply, Subsemiring.ringEquivOpMop_apply, CategoryTheory.Abelian.Ext.addEquivBiprod_symm_apply, coprodAssoc_apply_inl_inl, Unitization.antilipschitzWith_addEquiv, map_finsum, neg'_symm_apply, AddCon.quotientKerEquivOfRightInverse_apply, LinearEquiv.arrowCongrAddEquiv_apply, AddCon.comapQuotientEquivOfSurj_symm_mk', Finsupp.sumFinsuppAddEquivProdFinsupp_symm_inr, HahnSeries.addOppositeEquiv_symm_apply_coeff, val_neg_piAddUnits_symm_apply, Finsupp.curryAddEquiv_symm_apply, Finsupp.liftAddHom_symm_apply, CochainComplex.HomComplex.Cochain.leftShiftAddEquiv_symm_apply, eq_iff_eq_on_generator, IsPrimitiveRoot.zmodEquivZPowers_apply_coe_nat, AddSubmonoid.map_equiv_eq_comap_symm, AddAut.mulLeft_apply_symm_apply, eq_symm_apply, MonomialOrder.div, WeierstrassCurve.Jacobian.Point.toAffineAddEquiv_symm_apply, toEquiv_toLexAddEquiv, DFinsupp.liftAddHom_comp_single, MonomialOrder.lex_le_iff, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_precomp, addMonoidAlgebraAddEquivDirectSum_symm_apply, coprodCongr_symm_apply, finsuppUnique_symm_apply_apply, prodUnique_symm_apply, coe_mk, zmultiplesAddHom_apply, MonomialOrder.degree_sPolynomial_le, coprodComm_symm_apply, FreeAbelianGroup.liftAddEquiv_apply_apply, CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv_apply, Equiv.addEquiv_symm_apply, CategoryTheory.Adjunction.homAddEquiv_apply, SkewMonoidAlgebra.domCongr_apply, AddCon.comapQuotientEquivOfSurj_mk, WithLp.addEquiv_symm_apply, CochainComplex.HomComplex.Cocycle.rightShiftAddEquiv_apply, MonomialOrder.degree_sub_leadingTerm_lt_degree, AddChar.doubleDualEmb_doubleDualEquiv_symm_apply, toAddUnits_symm_apply, MonoidAlgebra.mapDomainAddEquiv_apply, CochainComplex.HomComplex.Cocycle.equivHomShift_comp_shift, HahnSeries.addOppositeEquiv_apply, LinearEquiv.arrowCongrAddEquiv_symm_apply, addMonoidAlgebraAddEquivDirectSum_apply, MonomialOrder.degree_monomial_le, Unitization.uniformity_eq_aux, SubAddAction.ofStabilizer.conjMap_comp_apply, MonomialOrder.degLex_single_lt_iff, AddUnits.coe_opEquiv_symm, ModuleCat.homAddEquiv_apply, CategoryTheory.Abelian.Ext.addEquivBiprod_apply_snd, Unitization.lipschitzWith_addEquiv, Subsemiring.mopRingEquivOp_symm_apply, MonomialOrder.degree_sub_LTerm_lt, MonomialOrder.sPolynomial_lt_of_degree_ne_zero_of_degree_eq, WeierstrassCurve.Projective.Point.toAffineAddEquiv_symm_apply, AlgEquiv.subalgebraMap_symm_apply_coe, coe_toAddHom, ModuleCat.semilinearMapAddEquiv_symm_apply_apply, coprodAssoc_symm_apply_inr_inl, map_sub, Nat.Partition.coeff_genFun, RestrictScalars.addEquiv_symm_map_algebraMap_smul, AddCircle.equivAddCircle_symm_apply_mk, AddAut.smul_def, AddSubsemigroup.centerToAddOpposite_apply_coe, CategoryTheory.Abelian.Ext.biprodAddEquiv_symm_apply, op_symm_apply_apply, RingEquiv.nonUnitalSubsemiringMap_apply_coe, AddAut.neg_conj_apply, CochainComplex.HomComplex.Cochain.toSingleEquiv_toSingleMk, starAddEquiv_apply, map_neg, DFinsupp.liftAddHom_symm_apply, addMonoidHomCongrRight_apply, toAddUnits_val_apply, AddChar.zmodAddEquiv_apply, AddCon.congr_mk, Subring.ringEquivOpMop_apply, piCongrRight_apply, groupHomology.H1AddEquivOfIsTrivial_symm_tmul, coe_toAddMonoidHom, AddCon.quotientKerEquivOfRightInverse_symm_apply, Matrix.coe_ofAddEquiv, CochainComplex.HomComplex.CohomologyClass.toHom_mk, AddAction.stabilizerEquivStabilizer_compTriple, uniqueProd_apply, IsPrimitiveRoot.zmodEquivZPowers_apply_coe_int, CochainComplex.HomComplex.Cocycle.leftShiftAddEquiv_apply, Multiset.toFinsupp_support, MulOpposite.opAddEquiv_symm_apply, ModuleCat.semilinearMapAddEquiv_apply, QuaternionAlgebra.coe_addEquivTuple, apply_eq_iff_symm_apply, CategoryTheory.Abelian.Ext.addEquivBiprod_apply_fst, AddSubmonoid.mem_map_equiv, coe_toLexAddEquiv, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, ofBijective_apply_symm_apply, AddAutAdditive_symm_apply_apply, val_piAddUnits_apply, Multiset.toFinsupp_strictMono, toFun_eq_coe, MonomialOrder.degree_sPolynomial_lt_sup_degree, ofLeftInverse_symm_apply, CochainComplex.HomComplex.Cocycle.equivHomShift_apply, AddCommGrpCat.homAddEquiv_apply, AddSubmonoid.topEquiv_toAddMonoidHom, MonomialOrder.degree_sub_leadingTerm_lt_iff, MonomialOrder.degree_sub_leadingTerm_le, Matrix.piAddEquiv_apply, AlternatingMap.domDomCongrEquiv_symm_apply, CategoryTheory.Abelian.Ext.biprodAddEquiv_apply_snd, WithLp.coe_symm_addEquiv, Matrix.compAddEquiv_symm_apply, AddSubmonoid.leftNegEquiv_symm_eq_neg, CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_symm_apply, Matrix.compAddEquiv_apply, LinearEquiv.coe_addEquiv_apply, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_zpow, op_apply_symm_apply, RestrictScalars.smul_def, toEquiv_ofLexAddEquiv, AddMonoidHom.ofInjective_apply, Subring.addEquivOp_symm_apply_coe, QuaternionAlgebra.coe_symm_addEquivTuple, comapAddSubgroup_symm_apply, Rep.indResHomEquiv_symm_apply_hom, punitCoprod_apply, Finsupp.toMultiset_eq_iff, AddAut.inv_apply_self, MonomialOrder.degree_sub_LTerm_le, MonomialOrder.lex_le_iff_of_unique, CochainComplex.HomComplex.CohomologyClass.homAddEquiv_apply, RestrictScalars.addEquiv_map_smul, CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_apply, AddSubmonoid.centerToAddOpposite_apply_coe, MultilinearMap.domDomCongrEquiv_apply, MonomialOrder.degree_sPolynomial, SemimoduleCat.homAddEquiv_symm_apply_hom, AddSubmonoid.LocalizationMap.addEquivOfLocalizations_apply, coe_symm_toIntLinearEquiv, MonomialOrder.degree_X_le_single, CategoryTheory.Iso.addCommGroupIsoToAddEquiv_apply, op_apply_apply, eq_symm_comp, SubAddAction.ofStabilizer.conjMap_apply, uliftZMultiplesHom_symm_apply
instInhabited 📖	CompOp	—
mk' 📖	CompOp	—
ofBijective 📖	CompOp	2 math math: ofBijective_apply, ofBijective_apply_symm_apply
refl 📖	CompOp	28 math math: RingEquiv.coe_addEquiv_refl, toIntLinearEquiv_refl, Finsupp.domCongr_refl, Finsupp.mapRange.addEquiv_refl, Int.univ_addEquiv, coe_addMonoidHom_refl, addMonoidHomCongrRightEquiv_refl, AddMonoidAlgebra.domCongr_refl, Int.addEquiv_eq_refl_or_neg, addMonoidHomCongrLeftEquiv_refl, coe_refl, withZeroCongr_refl, piCongrRight_refl, AddSubmonoid.LocalizationMap.ofAddEquivOfDom_id, DFinsupp.mapRange.addEquiv_refl, addMonoidHomCongrLeft_refl, toNatLinearEquiv_refl, refl_symm, QuotientAddGroup.equivQuotientZSMulOfEquiv_refl, refl_apply, AddAut.one_def, mapMatrix_refl, addMonoidHomCongrRight_refl, symm_trans_self, AddSubmonoid.LocalizationMap.ofAddEquivOfLocalizations_id, AddAction.stabilizerEquivStabilizer_zero, self_trans_symm, FreeAddGroup.freeAddGroupCongr_refl
symmEquiv 📖	CompOp	4 math math: symmEquiv_symm_apply_symm_apply, symmEquiv_apply_symm_apply, symmEquiv_symm_apply_apply, symmEquiv_apply_apply
toAddHom 📖	CompOp	7 math math: withZeroCongr_apply, toAddMagmaCatIso_inv, toAddSemigrpIso_hom, toAddHom_eq_coe, toAddMagmaCatIso_hom, coe_toAddHom, toAddSemigrpIso_inv
toAddMonoidHom 📖	CompOp	66 math math: AddSubmonoid.LocalizationMap.ofAddEquivOfLocalizations_eq, addMonoidHomCongrLeftEquiv_apply, toMultiplicative_apply_symm_apply, AddMonCat.uliftFunctor_map, toAddMonoidHom_eq_coe, toAddMonCatIso_hom, AddSubgroup.characteristic_iff_comap_le, toMultiplicativeRight_apply_apply, AddAction.stabilizer_vadd_eq_stabilizer_map_conj, coe_comapAddSubgroup, AddGrpCat.uliftFunctor_map, AddCommGrpCat.Colimits.colimitCocone_ι_app, AddSubgroup.characteristic_iff_le_map, toMultiplicativeLeft_apply_symm_apply, AddSubmonoid.subPairs_comap, toMultiplicativeRight_apply_symm_apply, DirectSum.coe_congr_addEquiv, map_dfinsuppSumAddHom, toAddMonCatIso_inv, toAddCommMonCatIso_inv, toAddGrpIso_hom, AddSubgroup.goursat_surjective, RingEquiv.toAddMonoidMom_commutes, AddSubgroup.exists_addEquiv_eq_graph, toAddCommGrpIso_hom, AddSubgroup.map_equiv_normalizer_eq, AddSubgroup.characteristic_iff_map_eq, SubAddAction.fixingAddSubgroup_vadd_eq_fixingAddSubgroup_map_conj, AddCommGrpCat.Colimits.Quot.desc_colimitCocone, AddSubgroup.comap_toAddSubmonoid, addMonoidHomCongrRightEquiv_symm_apply, toMultiplicative_apply_apply, AddSubgroup.map_equiv_eq_comap_symm', AddAction.IsBlock.of_addSubgroup_of_conjugate, AddMonoidHom.exists_addEquiv_mrange_eq_mgraph, addMonoidHomCongrLeftEquiv_symm_apply, LinearEquiv.map_dfinsuppSumAddHom, coe_mapAddSubgroup, AddSubgroup.characteristic_iff_le_comap, AddMonoidHom.mul_op_ext_iff, MulEquiv.toAdditive_symm_apply_apply, toAddMonoidHom_injective, AddSubmonoid.exists_addEquiv_eq_mgraph, AddSubgroup.mem_map_equiv, AddSubmonoid.LocalizationMap.ofAddEquivOfLocalizations_comp, AddSubgroup.Characteristic.fixed, toAddGrpIso_inv, AddCommGrpCat.uliftFunctor_map, addMonoidHomCongrRightEquiv_apply, Finsupp.mapRange.addEquiv_toAddMonoidHom, LinearEquiv.toAddMonoidHom_commutes, MulEquiv.toAdditive_symm_apply_symm_apply, AddCommGrpCat.Colimits.Quot.desc_quotQuotUliftAddEquiv, AddSubgroup.comap_equiv_eq_map_symm', DirectSum.coe_congrAddEquiv, SubAddAction.fixingAddSubgroup_map_conj_eq, AddMonoidHom.exists_addEquiv_range_eq_graph, AddSubgroup.goursat, coe_toAddMonoidHom, toAddCommGrpIso_inv, AddSubmonoid.mem_map_equiv, AddCommMonCat.uliftFunctor_map, AddSubgroup.characteristic_iff_comap_eq, toAddCommMonCatIso_hom, AddSubgroup.characteristic_iff_map_le, toMultiplicativeLeft_apply_apply
toEquiv 📖	CompOp	55 math math: CategoryTheory.Abelian.Ext.homLinearEquiv_apply, Representation.ofMulActionSelfAsModuleEquiv_symm_apply, addSubgroupMap_symm_apply, Finsupp.sumFinsuppLEquivProdFinsupp_apply, invFun_eq_symm, RingEquiv.toEquiv_commutes, LinearEquiv.domMulActCongrRight_symm_apply, starLinearEquiv_symm_apply, Multiset.Icc_eq, LinearEquiv.domMulActCongrRight_apply, LinearEquiv.congrLeft_symm_apply, MultilinearMap.domDomCongrLinearEquiv_symm_apply, toHomeomorph_toContinuousAddEquiv, ModuleCat.homLinearEquiv_symm_apply, SemimoduleCat.homLinearEquiv_apply, Matrix.conjTransposeLinearEquiv_apply, ContinuousAddEquiv.continuous_toFun, Matrix.piLinearEquiv_apply, Finsupp.sumFinsuppLEquivProdFinsupp_symm_apply, ContinuousAddEquiv.toEquiv_eq_coe, OrderAddMonoidIso.map_le_map_iff', Finset.mapRange_finsuppAntidiag_eq, add_submonoid_map_symm_apply, LinearEquiv.congrLeft_apply, ContinuousAddEquiv.continuous_invFun, MultilinearMap.domDomCongrLinearEquiv_apply, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_symm_apply, Multiset.uIcc_eq, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_apply, Matrix.uniqueLinearEquiv_apply, Representation.ofMulActionSelfAsModuleEquiv_apply, symm_map_add, Finset.mapRange_finsuppAntidiag_subset, addSubmonoidMap_symm_apply, OrderAddMonoidIso.toFun_eq_coe, sigmaFinsuppLequivDFinsupp_symm_apply, ContinuousAddEquiv.invFun_eq_symm, WithLp.linearEquiv_apply, toEquiv_injective, Matrix.uniqueLinearEquiv_symm_apply, toEquiv_eq_coe, map_add', LinearEquiv.prodAssoc_apply, ModuleCat.homLinearEquiv_apply, Matrix.transposeAlgEquiv_symm_apply, OrderAddMonoidIso.invFun_eq_symm, Matrix.piLinearEquiv_symm_apply, WithLp.linearEquiv_symm_apply, CategoryTheory.Abelian.Ext.homLinearEquiv_symm_apply, SemimoduleCat.homLinearEquiv_symm_apply, toFun_eq_coe, Matrix.transposeLinearEquiv_apply, DirectSum.lequivProdDirectSum_symm_apply, DirectSum.lequivProdDirectSum_apply, sigmaFinsuppLequivDFinsupp_apply
trans 📖	CompOp	35 math math: toIntLinearEquiv_trans, QuotientAddGroup.equivQuotientZSMulOfEquiv_trans, AddMonoidAlgebra.mapRangeAddEquiv_trans, mapMatrix_trans, OrderAddMonoidIso.coe_trans_addEquiv, mulOp_symm_apply, toNatLinearEquiv_trans, MonoidAlgebra.mapDomainAddEquiv_trans, mulOp_apply, coe_trans, MonoidAlgebra.mapRangeAddEquiv_trans, AddMonoidAlgebra.mapDomainRingEquiv_trans, withZeroCongr_trans, coe_addMonoidHom_trans, addMonoidHomCongrLeft_trans, addMonoidHomCongrRight_trans, FreeAddGroup.freeAddGroupCongr_trans, symm_trans_apply, AddSubmonoid.LocalizationMap.ofAddEquivOfLocalizations_comp, AddAction.stabilizerEquivStabilizer_trans, piCongrRight_trans, addMonoidHomCongrRightEquiv_trans, Matrix.transposeAlgEquiv_symm_apply, trans_apply, addMonoidHomCongrLeftEquiv_trans, DFinsupp.mapRange.addEquiv_trans, RingEquiv.coe_addEquiv_trans, AddMonoidAlgebra.mapDomainAddEquiv_trans, Finsupp.domCongr_trans, Finsupp.mapRange.addEquiv_trans, symm_trans_self, AddAut.mul_def, AddAut.congr_apply, self_trans_symm, AddAut.congr_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eq_iff_eq 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike	—	injective
apply_eq_iff_symm_apply 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.apply_eq_iff_eq_symm_apply
apply_symm_apply 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.apply_symm_apply
bijective 📖	mathematical	—	Function.Bijective DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike	—	EquivLike.bijective
cast_apply 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike cast	—	—
cast_symm_apply 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike symm cast	—	—
coe_addMonoidHom_comp_coe_addMonoidHom_symm 📖	mathematical	—	AddMonoidHom.comp AddZeroClass.toAddZero AddMonoidHomClass.toAddMonoidHom AddEquiv AddZero.toAdd EquivLike.toFunLike instEquivLike AddEquivClass.instAddMonoidHomClass instAddEquivClass symm AddMonoidHom.id	—	AddMonoidHom.ext AddEquivClass.instAddMonoidHomClass instAddEquivClass apply_symm_apply
coe_addMonoidHom_refl 📖	mathematical	—	AddMonoidHomClass.toAddMonoidHom AddEquiv AddZero.toAdd AddZeroClass.toAddZero EquivLike.toFunLike instEquivLike AddEquivClass.instAddMonoidHomClass instAddEquivClass refl AddMonoidHom.id	—	AddEquivClass.instAddMonoidHomClass instAddEquivClass
coe_addMonoidHom_symm_comp_coe_addMonoidHom 📖	mathematical	—	AddMonoidHom.comp AddZeroClass.toAddZero AddMonoidHomClass.toAddMonoidHom AddEquiv AddZero.toAdd EquivLike.toFunLike instEquivLike AddEquivClass.instAddMonoidHomClass instAddEquivClass symm AddMonoidHom.id	—	AddMonoidHom.ext AddEquivClass.instAddMonoidHomClass instAddEquivClass symm_apply_apply
coe_addMonoidHom_trans 📖	mathematical	—	AddMonoidHomClass.toAddMonoidHom AddEquiv AddZero.toAdd AddZeroClass.toAddZero EquivLike.toFunLike instEquivLike AddEquivClass.instAddMonoidHomClass instAddEquivClass trans AddMonoidHom.comp	—	AddEquivClass.instAddMonoidHomClass instAddEquivClass
coe_mk 📖	mathematical	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	AddEquiv instEquivLike	—	—
coe_refl 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike refl	—	—
coe_toAddHom 📖	mathematical	—	DFunLike.coe AddHom AddHom.funLike toAddHom AddEquiv EquivLike.toFunLike instEquivLike	—	—
coe_toAddMonoidHom 📖	mathematical	—	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoidHom.instFunLike toAddMonoidHom AddEquiv AddZero.toAdd EquivLike.toFunLike instEquivLike	—	—
coe_toEquiv 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike EquivLike.toEquiv AddEquiv instEquivLike	—	—
coe_toEquiv_symm 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm EquivLike.toEquiv AddEquiv instEquivLike symm	—	—
coe_trans 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike trans	—	—
comp_left_injective 📖	mathematical	—	AddMonoidHom AddZeroClass.toAddZero AddMonoidHom.comp AddMonoidHomClass.toAddMonoidHom AddEquiv AddZero.toAdd EquivLike.toFunLike instEquivLike AddEquivClass.instAddMonoidHomClass instAddEquivClass	—	AddEquivClass.instAddMonoidHomClass instAddEquivClass coe_addMonoidHom_comp_coe_addMonoidHom_symm AddMonoidHom.comp_id
comp_right_injective 📖	mathematical	—	AddMonoidHom AddZeroClass.toAddZero AddMonoidHom.comp AddMonoidHomClass.toAddMonoidHom AddEquiv AddZero.toAdd EquivLike.toFunLike instEquivLike AddEquivClass.instAddMonoidHomClass instAddEquivClass	—	AddEquivClass.instAddMonoidHomClass instAddEquivClass coe_addMonoidHom_symm_comp_coe_addMonoidHom AddMonoidHom.id_comp
comp_symm_eq 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.comp_symm_eq
congr_arg 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike	—	DFunLike.congr_arg
congr_fun 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike	—	DFunLike.congr_fun
eq_comp_symm 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.eq_comp_symm
eq_symm_apply 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.eq_symm_apply
eq_symm_comp 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.eq_symm_comp
equivLike_neg_eq_symm 📖	mathematical	—	EquivLike.inv AddEquiv instEquivLike DFunLike.coe EquivLike.toFunLike symm	—	—
ext 📖	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike	—	ext
injective 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike	—	EquivLike.injective
instAddEquivClass 📖	mathematical	—	AddEquivClass AddEquiv instEquivLike	—	map_add'
invFun_eq_symm 📖	mathematical	—	Equiv.invFun toEquiv DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike symm	—	—
map_add 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike	—	map_add AddEquivClass.instAddHomClass instAddEquivClass
map_add' 📖	mathematical	—	Equiv.toFun toEquiv	—	—
map_eq_zero_iff 📖	mathematical	—	DFunLike.coe AddEquiv AddZero.toAdd AddZeroClass.toAddZero EquivLike.toFunLike instEquivLike AddZero.toZero	—	EmbeddingLike.map_eq_zero_iff EquivLike.toEmbeddingLike AddMonoidHomClass.toZeroHomClass AddEquivClass.instAddMonoidHomClass instAddEquivClass
map_ne_zero_iff 📖	—	—	—	—	EmbeddingLike.map_ne_zero_iff EquivLike.toEmbeddingLike AddMonoidHomClass.toZeroHomClass AddEquivClass.instAddMonoidHomClass instAddEquivClass
map_neg 📖	mathematical	—	DFunLike.coe AddEquiv AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SubtractionMonoid.toSubNegMonoid EquivLike.toFunLike instEquivLike SubNegMonoid.toNeg	—	map_neg AddEquivClass.instAddMonoidHomClass instAddEquivClass
map_sub 📖	mathematical	—	DFunLike.coe AddEquiv AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SubtractionMonoid.toSubNegMonoid EquivLike.toFunLike instEquivLike SubNegMonoid.toSub	—	map_sub AddEquivClass.instAddMonoidHomClass instAddEquivClass
map_zero 📖	mathematical	—	DFunLike.coe AddEquiv AddZero.toAdd AddZeroClass.toAddZero EquivLike.toFunLike instEquivLike AddZero.toZero	—	map_zero AddMonoidHomClass.toZeroHomClass AddEquivClass.instAddMonoidHomClass instAddEquivClass
mk_coe 📖	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike Equiv.toFun	—	—	ext
mk_coe' 📖	mathematical	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike Equiv.toFun	symm	—	Function.Bijective.injective symm_bijective ext
ofBijective_apply 📖	mathematical	Function.Bijective DFunLike.coe	AddEquiv EquivLike.toFunLike instEquivLike ofBijective	—	—
ofBijective_apply_symm_apply 📖	mathematical	Function.Bijective DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoidHom.instFunLike	AddEquiv AddZero.toAdd EquivLike.toFunLike instEquivLike symm ofBijective AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass	—	apply_symm_apply AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass
refl_apply 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike refl	—	—
refl_symm 📖	mathematical	—	symm refl	—	—
self_comp_symm 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike symm	—	apply_symm_apply
self_trans_symm 📖	mathematical	—	trans symm refl	—	DFunLike.ext symm_apply_apply
surjective 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike	—	EquivLike.surjective
symmEquiv_apply_apply 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike Equiv Equiv.instEquivLike symmEquiv symm	—	—
symmEquiv_apply_symm_apply 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike symm Equiv Equiv.instEquivLike symmEquiv	—	—
symmEquiv_symm_apply_apply 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike Equiv Equiv.instEquivLike Equiv.symm symmEquiv symm	—	—
symmEquiv_symm_apply_symm_apply 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike symm Equiv Equiv.instEquivLike Equiv.symm symmEquiv	—	—
symm_apply_apply 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.symm_apply_apply
symm_apply_eq 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.symm_apply_eq
symm_bijective 📖	mathematical	—	Function.Bijective AddEquiv symm	—	Function.bijective_iff_has_inverse symm_symm
symm_comp_eq 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.symm_comp_eq
symm_comp_self 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike symm	—	symm_apply_apply
symm_map_add 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm toEquiv	—	map_add AddHom.addHomClass Equiv.left_inv Equiv.right_inv
symm_mk 📖	mathematical	Equiv.toFun	symm Equiv.symm symm_map_add	—	—
symm_symm 📖	mathematical	—	symm	—	—
symm_trans_apply 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike symm trans	—	—
symm_trans_self 📖	mathematical	—	trans symm refl	—	DFunLike.ext apply_symm_apply
toAddHom_eq_coe 📖	mathematical	—	toAddHom AddHomClass.toAddHom AddEquiv EquivLike.toFunLike instEquivLike AddEquivClass.instAddHomClass instAddEquivClass	—	—
toAddMonoidHom_eq_coe 📖	mathematical	—	toAddMonoidHom AddMonoidHomClass.toAddMonoidHom AddEquiv AddZero.toAdd AddZeroClass.toAddZero EquivLike.toFunLike instEquivLike AddEquivClass.instAddMonoidHomClass instAddEquivClass	—	—
toAddMonoidHom_injective 📖	mathematical	—	AddEquiv AddZero.toAdd AddZeroClass.toAddZero AddMonoidHom toAddMonoidHom	—	Function.Injective.of_comp DFunLike.coe_injective
toEquiv_eq_coe 📖	mathematical	—	toEquiv EquivLike.toEquiv AddEquiv instEquivLike	—	—
toEquiv_injective 📖	mathematical	—	AddEquiv Equiv toEquiv	—	—
toEquiv_symm 📖	mathematical	—	EquivLike.toEquiv AddEquiv instEquivLike symm Equiv.symm	—	—
toFun_eq_coe 📖	mathematical	—	Equiv.toFun toEquiv DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike	—	—
trans_apply 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike instEquivLike trans	—	—

AddEquiv.Simps

Definitions

Name	Category	Theorems
symm_apply 📖	CompOp	—

AddEquivClass

Definitions

Name	Category	Theorems
toAddEquiv 📖	CompOp	41 math math: LinearEquiv.coe_toAddEquiv, RingEquiv.coe_addEquiv_refl, AddEquiv.toIntLinearEquiv_toAddEquiv, RingEquiv.toEquiv_commutes, apply_coe_symm_apply, RingEquiv.op_apply_symm_apply, MulOpposite.coe_opLinearEquiv_symm_addEquiv, coe_symm_apply_apply, AddEquiv.toNatLinearEquiv_toAddEquiv, MulOpposite.coe_opLinearEquiv_addEquiv, AlgEquiv.op_apply_symm_apply, AddEquiv.toAddEquiv_toContinuousAddEquiv, OrderAddMonoidIso.coe_trans_addEquiv, OrderAddMonoidIso.coe_addEquiv, RingEquiv.toAddMonoidMom_commutes, LinearEquiv.coe_toAddEquiv_symm, RingEquiv.coe_toAddEquiv, AddSubmonoid.map_coe_toAddEquiv, AddGroupExtension.Equiv.coe_symm, AlgEquiv.symm_toAddEquiv, OrderAddMonoidIso.toAddEquiv_eq_coe, AlgEquiv.op_symm_apply_symm_apply, AlternatingMap.domDomCongrₗ_toAddEquiv, RingEquiv.op_symm_apply_symm_apply, RingEquiv.nonUnitalSubsemiringMap_symm_apply_coe, ContinuousAddEquiv.toAddEquiv_eq_coe, RingEquiv.toAddEquiv_eq_coe, AddGroupExtension.Equiv.toAddEquiv_eq_coe, ContinuousMap.linearIsometryBoundedOfCompact_toAddEquiv, AddGroupExtension.Equiv.coe_toAddEquiv, AlgEquiv.opComm_symm_apply_symm_apply, RingEquiv.coe_addEquiv_trans, RingEquiv.coe_toAddEquiv_symm, LinearEquiv.toAddEquiv_toNatLinearEquiv, AddSubgroup.addSubgroupOfContinuousAddEquivOfLe_toAddEquiv, AlgEquiv.subalgebraMap_symm_apply_coe, RingEquiv.prodProdProdComm_toAddEquiv, toAddEquiv_injective, LinearEquiv.toAddEquiv_toIntLinearEquiv, LinearEquiv.coe_addEquiv_apply, LinearEquiv.prodProdProdComm_toAddEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_coe_symm_apply 📖	mathematical	—	DFunLike.coe EquivLike.toFunLike AddEquiv AddEquiv.instEquivLike AddEquiv.symm toAddEquiv	—	Equiv.right_inv
coe_symm_apply_apply 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm toAddEquiv	—	Equiv.left_inv
instAddHomClass 📖	mathematical	—	AddHomClass EquivLike.toFunLike	—	map_add
instAddMonoidHomClass 📖	mathematical	—	AddMonoidHomClass AddZeroClass.toAddZero EquivLike.toFunLike	—	instAddHomClass add_zero EquivLike.right_inv map_add zero_add
map_add 📖	mathematical	—	DFunLike.coe EquivLike.toFunLike	—	—
map_eq_zero_iff 📖	mathematical	—	DFunLike.coe	—	EmbeddingLike.map_eq_zero_iff
map_ne_zero_iff 📖	—	—	—	—	EmbeddingLike.map_ne_zero_iff

AddHom

Definitions

Name	Category	Theorems
toAddEquiv 📖	CompOp	2 math math: toAddEquiv_apply, toAddEquiv_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toAddEquiv_apply 📖	mathematical	comp id	DFunLike.coe AddEquiv EquivLike.toFunLike AddEquiv.instEquivLike toAddEquiv AddHom funLike	—	—
toAddEquiv_symm_apply 📖	mathematical	comp id	DFunLike.coe AddEquiv EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm toAddEquiv AddHom funLike	—	—

AddMonoidHom

Definitions

Name	Category	Theorems
toAddEquiv 📖	CompOp	2 math math: toAddEquiv_symm_apply, toAddEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toAddEquiv_apply 📖	mathematical	comp AddZeroClass.toAddZero id	DFunLike.coe AddEquiv AddZero.toAdd EquivLike.toFunLike AddEquiv.instEquivLike toAddEquiv AddMonoidHom instFunLike	—	—
toAddEquiv_symm_apply 📖	mathematical	comp AddZeroClass.toAddZero id	DFunLike.coe AddEquiv AddZero.toAdd EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm toAddEquiv AddMonoidHom instFunLike	—	—

EmbeddingLike

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_eq_one_iff 📖	mathematical	—	DFunLike.coe	—	map_eq_one_iff injective
map_eq_zero_iff 📖	mathematical	—	DFunLike.coe	—	map_eq_zero_iff injective
map_ne_one_iff 📖	—	—	—	—	Iff.not map_eq_one_iff
map_ne_zero_iff 📖	—	—	—	—	Iff.not map_eq_zero_iff

MonoidHom

Definitions

Name	Category	Theorems
toMulEquiv 📖	CompOp	2 math math: toMulEquiv_symm_apply, toMulEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toMulEquiv_apply 📖	mathematical	comp MulOneClass.toMulOne id	DFunLike.coe MulEquiv MulOne.toMul EquivLike.toFunLike MulEquiv.instEquivLike toMulEquiv MonoidHom instFunLike	—	—
toMulEquiv_symm_apply 📖	mathematical	comp MulOneClass.toMulOne id	DFunLike.coe MulEquiv MulOne.toMul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm toMulEquiv MonoidHom instFunLike	—	—

MulEquiv

Definitions

Name	Category	Theorems
cast 📖	CompOp	2 math math: cast_symm_apply, cast_apply
instCoeFunForall 📖	CompOp	—
instEquivLike 📖	CompOp	701 math math: MonoidAlgebra.mapDomainRingEquiv_single, Submonoid.mem_map_equiv, ConjAct.smul_def, SubMulAction.ofStabilizer.conjMap_comp_apply, FreeMonoid.freeMonoidCongr_of, SubMulAction.ofFixingSubgroup_insert_map_apply, ContinuousLinearEquiv.unitsEquiv_apply, ConjAct.toConjAct_inv, ValuationSubring.coe_mem_principalUnitGroup_iff, Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_apply, galRestrict_symm_algebraMap_apply, Subgroup.equivSMul_apply_coe, map_eq_one_iff, MulAut.one_apply, ConjAct.toConjAct_mul, FreeGroupBasis.repr_apply_coe, Ideal.exists_comap_galRestrict_eq, coe_trans, Subgroup.centerCongr_symm_apply_coe, zpowersMulHom_symm_apply, monoidHomCongrLeft_apply, rootsOfUnityEquivOfPrimitiveRoots_apply_coe_inv_val, CategoryTheory.Iso.conjAut_apply, AddEquiv.toMultiplicative_apply_symm_apply, coe_monoidHom_symm_comp_coe_monoidHom, autAdjoinRootXPowSubCEquiv_root, CoxeterMatrix.reindex_relationsSet, Subgroup.equivMapOfInjective_coe_mulEquiv, MonoidHom.restrictHomKerEquiv_apply_coe, NumberField.IsCMField.unitsComplexConj_torsion, ConjAct.stabilizer_eq_centralizer, inv'_apply, Subgroup.comap_equiv_eq_map_symm, WithZero.withZeroUnitsEquiv_symm_apply_coe, mulEquivOfOrderOfEq_symm_apply_gen, prodProdProdComm_apply, AddAutAdditive_apply_symm_apply, MulAut.inv_apply, Submonoid.mul_leftInvEquiv, CategoryTheory.InducedCategory.endEquiv_symm_apply_hom, StarMulEquiv.coe_mk, CategoryTheory.InducedCategory.endEquiv_apply, MulAut.conjNormal_symm_apply, Ideal.coe_smul_primesOver_mk_eq_map_galRestrict, SubMulAction.ofStabilizer.conjMap_comp_inv_apply, WithZero.coe_unitsWithZeroEquiv_eq_units_val, val_inv_unitarySubgroupUnitsEquiv_symm_apply_coe, Submonoid.leftInvEquiv_symm_mul, Subsemigroup.centerToMulOpposite_apply_coe, CategoryTheory.Iso.commGroupIsoToMulEquiv_symm_apply, OrderMonoidIso.withZero_symm_apply_symm_apply, IsCyclic.val_mulAutMulEquiv_apply, CongruenceSubgroup.exists_Gamma_le_conj', Unitary.conjStarAlgEquiv_unitaryLinearIsometryEquiv, unitsNonZeroDivisorsEquiv_apply, symm_comp_self, AddEquiv.toMultiplicativeRight_apply_apply, Submonoid.fromLeftInv_leftInvEquiv_symm, MulAction.stabilizerEquivStabilizer_symm_apply, CongruenceSubgroup.conjGL_coe, map_one, Subgroup.isCoatom_map, associatesEquivOfUniqueUnits_symm_apply, SemidirectProduct.inl_aut, piMultiplicative_apply, Subsemigroup.centerCongr_symm_apply_coe, OrderMonoidIso.val_unitsCongr_symm_apply, Submonoid.LocalizationMap.mulEquivOfLocalizations_apply, eq_symm_apply, Subgroup.comap_toSubmonoid, InfiniteGalois.normalAutEquivQuotient_apply, CategoryTheory.Functor.FullyFaithful.homMulEquiv_apply, IsGaloisGroup.mulEquivAlgEquiv_apply_symm_apply, MonoidAlgebra.domCongr_toAlgHom, Set.unitEquivUnitsInteger_symm_apply_coe, Equiv.Perm.val_equivUnitsEnd_apply, CategoryTheory.PreGaloisCategory.toAutMulEquiv_isHomeomorph, Localization.mulEquivOfQuotient_symm_monoidOf, CategoryTheory.Iso.refl_conj, val_unitarySubgroupUnitsEquiv_symm_apply_coe, comapSubgroup_symm_apply, toEquiv_toLexMulEquiv, MulDistribMulAction.toMulEquiv_apply, autEquivZmod_symm_apply_natCast, Matrix.GeneralLinearGroup.coe_toLin, toMonoidHom_eq_coe, map_dvd_iff_dvd_symm, toSingleObjEquiv_inverse_map, Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_symm_apply_coe_coe, NonUnitalSubsemiring.centerCongr_symm_apply_coe, CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_symm_apply_hom, autAdjoinRootXPowSubCEquiv_symm_smul, MonoidHom.ofLeftInverse_symm_apply, AddAutAdditive_apply_apply, AddOpposite.opMulEquiv_symm_apply, SubMulAction.ofStabilizer.inv_conjMap_comp_apply, Unitary.coe_linearIsometryEquiv_apply, coe_refl, ConjAct.forall, HNNExtension.equiv_eq_conj, LinearMap.GeneralLinearGroup.generalLinearEquiv_to_linearMap, uliftZPowersHom_symm_apply, map_div, AddAutAdditive_symm_apply_symm_apply, CategoryTheory.Iso.conj_pow, Subsemiring.centerCongr_symm_apply_coe, Unitary.linearIsometryEquiv_coe_apply, CategoryTheory.Iso.conjAut_mul, MulAut.smul_def, coe_submonoidMap_apply, prodMultiplicative_symm_apply, val_piUnits_symm_apply, val_unitsCentralizerEquiv_apply_coe, SpecialLinearGroup.centerCongr_toLin_equiv_trans_centerEquivRootsOfUnity_eq, Equiv.altCongrHom_apply_coe, RingEquiv.coe_toMulEquiv, Submonoid.equivMapOfInjective_coe_mulEquiv, IsCusp.of_isFiniteRelIndex_conj, ConjAct.toConjAct_zero, MulAutMultiplicative_symm_apply_apply, MulAut.mul_apply, opOp_symm_apply, comp_symm_eq, mapSubgroup_apply, op_apply_symm_apply, map_finprod, RootPairing.Equiv.toEndUnit_inv, comp_right_injective, apply_eq_iff_eq, ZMod.AddAutEquivUnits_symm_apply, starMulAut_apply, HNNExtension.inv_t_mul_of, QuotientGroup.liftEquiv_coe, eq_symm_comp, MulAutMultiplicative_apply_apply, Submonoid.LocalizationMap.ofMulEquivOfDom_comp_symm, MulAut.inv_apply_self, SlashInvariantForm.coe_translate, Submonoid.topEquiv_symm_apply_coe, Subgroup.coe_equivMapOfInjective_apply, AddEquiv.toMultiplicativeLeft_apply_symm_apply, Submonoid.map_coe_toMulEquiv, QuotientGroup.quotientKerEquivOfRightInverse_apply, Equiv.permCongrHom_coe, coe_galRestrict_apply, ModularGroup.lcRow0Extend_symm_apply, Subgroup.conjAct_pointwise_smul_iff, coprodPUnit_symm_apply, MulAction.stabilizerEquivStabilizer_compTriple, invFun_eq_symm, CoxeterSystem.getElem_succ_leftInvSeq_alternatingWord, OrderMonoidIso.coe_mulEquiv, CategoryTheory.Aut.toEnd_apply, AffineEquiv.linear_equivUnitsAffineMap_symm_apply, uliftPowersHom_symm_apply, coprodAssoc_symm_apply_inr_inr, Subgroup.centerCongr_apply_coe, Monoid.IsTorsion.torsionMulEquiv_apply, prodMultiplicative_apply, Subgroup.mem_map_equiv, unitarySubgroupUnitsEquiv_apply_coe, Submonoid.centerToMulOpposite_apply_coe, AddEquiv.toMultiplicativeRight_apply_symm_apply, zpowersMulHom_apply, Subsemigroup.topEquiv_symm_apply_coe, val_toUnits_apply, MulAut.coe_inv, instMulEquivClass, MonoidAlgebra.domCongr_single, unitary.linearIsometryEquiv_coe_symm_apply, withZero_apply_symm_apply, QuotientGroup.liftEquiv_mk, MulAut.coe_one, subgroupCongr_apply, SemidirectProduct.congr'_apply_right, OrderMonoidIso.val_inv_unitsCongr_symm_apply, lipschitzGroup.conjAct_smul_ι_mem_range_ι, FreeGroupBasis.lift_apply_apply, Subgroup.centerToMulOpposite_apply_coe, ofLeftInverse_symm_apply, CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_apply_inv, spinGroup.units_involute_act_eq_conjAct, Semigrp.mulEquiv_coe_eq, CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_apply_hom, IsGaloisGroup.mulEquivCongr_apply_smul, Con.comapQuotientEquivOfSurj_symm_mk', Subgroup.Commensurable.commensurator_mem_iff, Subgroup.map_symm_eq_iff_map_eq, algebraMap_galRestrict_apply, val_inv_unitsNonZeroDivisorsEquiv_symm_apply_coe, spinGroup.conjAct_smul_ι_mem_range_ι, comap_upperCentralSeries, Unitary.coe_symm_linearIsometryEquiv_apply, CategoryTheory.Iso.trans_conjAut, Submonoid.leftInvEquiv_apply, toMonoidWithZeroHom_apply, MulAutMultiplicative_symm_apply_symm_apply, toSingleObjEquiv_unitIso_hom, strictMono_subsemigroupCongr, Equiv.mulEquiv_apply, OrderMonoidIso.coe_mk, Submonoid.val_inv_unitsTypeEquivIsUnitSubmonoid_symm_apply, coprodPUnit_apply, Nonneg.val_unitsEquivPos_symm_apply_coe, spinGroup.conjAct_smul_range_ι, SpecialLinearGroup.congr_linearEquiv_coe_apply, ConjAct.ofConjAct_zero, MonoidHom.restrictHomKerEquiv_symm_coe_apply, monoidEndToAdditive_apply_apply, eq_comp_symm, CategoryTheory.Functor.map_conj, withZero_apply_apply, Con.comapQuotientEquivOfSurj_mk, CategoryTheory.Functor.map_conjAut, GrpWithZero.Iso.mk_hom, coe_prodAssoc, InfiniteGalois.mulEquivToLimit_symm_continuous, CongruenceSubgroup.IsArithmetic.conj, IsCyclic.val_inv_mulAutMulEquiv_apply, Subsemigroup.topEquiv_toMulHom, arrowCongr_apply, WithZero.withZeroUnitsEquiv_symm_strictMono, ModularGroup.lcRow0Extend_apply, coprodAssoc_apply_inl_inl, Monoid.PushoutI.NormalWord.cons_head, Submonoid.leftInvEquiv_mul, restrictRootsOfUnity_coe_apply, prodUnique_symm_apply, Localization.mulEquivOfQuotient_mk, OrderMonoidIso.withZero_apply_symm_apply, MulAction.stabilizerEquivStabilizer_apply, coe_prodComm_symm, InfiniteGalois.isOpen_mulEquivToLimit_image_fixingSubgroup, associatesNonZeroDivisorsEquiv_mk_mk, map_inv, WithZero.unitsWithZeroEquiv_symm_apply, ValuationSubring.coe_unitGroupMulEquiv_apply, Subgroup.subgroupOfEquivOfLe_symm_apply_coe_coe, autEquivZmod_symm_apply_intCast, ConjAct.units_smul_def, AffineEquiv.val_equivUnitsAffineMap_apply, MonoidHom.toMulEquiv_symm_apply, CategoryTheory.PreGaloisCategory.toAutMulEquiv_apply, MulOpposite.coe_symm_opMulEquiv, associatesNonZeroDivisorsEquiv_symm_mk_mk, IsGalois.normalAutEquivQuotient_apply, UniqueFactorizationMonoid.normalizedFactorsEquiv_symm_apply, val_inv_piUnits_apply, apply_eq_iff_symm_apply, CategoryTheory.SingleObj.toEnd_def, Matrix.GeneralLinearGroup.toLin'_apply, IsFreeGroup.toFreeGroup_symm_apply, CongruenceSubgroup.isArithmetic_conj_SL2Z, QuotientGroup.quotientKerEquivOfRightInverse_symm_apply, Submonoid.unitsTypeEquivIsUnitSubmonoid_apply_coe, WithZero.toMulBot_lt, HNNExtension.NormalWord.unitsSMul_one_group_smul, coe_ofLexMulEquiv, self_comp_symm, coprodAssoc_apply_inl_inr, SemidirectProduct.congr'_apply_left, CoxeterSystem.rightInvSeq_concat, IsGaloisGroup.mulEquivAlgEquiv_apply_apply, symm_apply_eq, toSingleObjEquiv_counitIso_hom, MulAut.coe_mul, withOneCongr_apply, SpecialLinearGroup.centerEquivRootsOfUnity_symm_apply, coe_toMonoidHom, pinGroup.conjAct_smul_ι_mem_range_ι, Unitization.val_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, SemidirectProduct.congr'_symm_apply_right, AddMonoid.End_apply, ofLeftInverse'_apply, mkFactorOrderIsoOfFactorDvdEquiv_apply_coe, Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, val_unitsNonZeroDivisorsEquiv_symm_apply_coe, NonUnitalSubring.centerCongr_symm_apply_coe, SemidirectProduct.mul_def, prodUnique_apply, ZMod.AddAutEquivUnits_apply, Subgroup.val_centerUnitsEquivUnitsCenter_symm_apply_coe, prodProdProdComm_toEquiv, coprodCongr_apply, Monoid.IsTorsion.torsionMulEquiv_symm_apply_coe, MulHom.toMulEquiv_symm_apply, Submonoid.centerToMulOpposite_symm_apply_coe, mulAutArrow_apply_apply, CategoryTheory.Functor.FullyFaithful.mulEquivEnd_symm_apply, ofLeftInverse_apply, Localization.mulEquivOfQuotient_mk', toMultiplicative_toAdditive_symm_apply, Subsemigroup.strictMono_topEquiv, CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_symm_app, MonoidAlgebra.toRingHom_mapDomainRingEquiv, HNNExtension.of_mul_t, congr_fun, Subgroup.topEquiv_symm_apply_coe, Unitary.linearIsometryEquiv_coe_symm_apply, Subgroup.normalizerMonoidHom_apply_apply_coe, congr_arg, CuspForm.coe_translate, HNNExtension.of_mul_inv_t, OrderMonoidIso.withZero_apply_apply, surjective, toSingleObjEquiv_unitIso_inv, Set.val_unitEquivUnitsInteger_apply_coe, WithZero.toMulBot_coe_ofAdd, Submonoid.LocalizationMap.ofMulEquivOfDom_comp, SubMulAction.ofFixingSubgroup_of_eq_apply, MulOpposite.opMulEquiv_apply, Ideal.Quotient.stabilizerQuotientInertiaEquiv_mk, cast_symm_apply, IsCyclotomicExtension.Rat.galEquivZMod_apply_of_pow_eq, Con.quotientKerEquivOfRightInverse_symm_apply, Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_apply, trans_apply, mulAutArrow_apply_symm_apply, Units.coe_unop_opEquiv, mapSubgroup_symm_apply, ext_iff, SemidirectProduct.inl_aut_inv, Subgroup.mem_ofUnits_iff_toUnits_mem, LinearMap.GeneralLinearGroup.congrLinearEquiv_apply, inv'_symm_apply, starMulEquiv_apply, Units.toAut_hom, equivLike_inv_eq_symm, CategoryTheory.Groupoid.vertexGroupIsomOfMap_apply, MulAut.conj_apply, ofBijective_apply_symm_apply, op_apply_apply, CategoryTheory.Hom.mulEquivCongrRight_symm_apply, toFun_eq_coe, uniqueProd_symm_apply, multiplicativeAdditive_apply, Submonoid.centerCongr_symm_apply_coe, MagmaCat.mulEquiv_coe_eq, AffineEquiv.equivUnitsAffineMap_symm_apply_apply, AddEquiv.toMultiplicative_apply_apply, Unitary.toAlgEquiv_conjStarAlgAut, coe_mk, groupCohomology.exists_mul_galRestrict_of_norm_eq_one, GroupExtension.Equiv.rightHom_comm, Nonneg.unitsEquivPos_apply_coe, surjective_rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar, toSingleObjEquiv_counitIso_inv, galRestrictHom_symm_algebraMap_apply, freeGroupEquivCoprodI_symm_apply, Con.comapQuotientEquivOfSurj_symm_mk, GroupExtension.Equiv.inl_comm, Matrix.SpecialLinearGroup.toLin_equiv.symm_toLinearMap_eq, ConjAct.toConjAct_smul, MulHom.toMulEquiv_apply, Subsemigroup.centerToMulOpposite_symm_apply_coe, pinGroup.conjAct_smul_range_ι, toEquiv_eq_coe, IsCyclotomicExtension.Rat.galEquivZMod_restrictNormal_apply, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply, MulDistribMulAction.toMulEquiv_symm_apply, NumberField.RingOfIntegers.withValEquiv_apply, Localization.mulEquivOfQuotient_symm_mk, AddOpposite.opMulEquiv_toEquiv, val_unitsCentralizerEquiv_symm_apply_coe, CoxeterMatrix.reindexGroupEquiv_apply_simple, Submodule.unitsQuotEquivRelPic_symm_apply, coprodAssoc_apply_inr, HNNExtension.t_mul_of, Subgroup.val_centerUnitsEquivUnitsCenter_apply_coe, symmEquiv_apply_apply, WithZero.toMonoidWithZeroHom_withZeroUnitsEquiv, MulAut.conj_inv_apply, AlgEquiv.algHomUnitsEquiv_apply_symm_apply, powersMulHom_apply, AddConstEquiv.coe_val_inv_equivUnits_apply, funUnique_symm_apply, uniqueProd_apply, comapSubgroup_apply, WithZero.toMulBot_zero, AlgEquiv.val_algHomUnitsEquiv_symm_apply, CategoryTheory.Functor.FullyFaithful.homMulEquiv_symm_apply, Submonoid.map_equiv_eq_comap_symm, eq_iff_eq_on_generator, CategoryTheory.yonedaGrpObjIsoOfRepresentableBy_hom, submonoidMap_symm_apply, Unitary.toRingEquiv_conjStarAlgAut, CategoryTheory.yonedaGrpObjIsoOfRepresentableBy_inv, FGModuleCat.Iso.conj_eq_conj, Set.conj_mem_fixingSubgroup, Submonoid.LocalizationMap.mulEquivOfLocalizations_symm_apply, monoidEndToAdditive_symm_apply_apply, SemidirectProduct.mulEquivProd_symm_apply_left, MonoidAlgebra.domCongr_comp_lsingle, symm_trans_apply, ContinuousMulEquiv.coe_mk, punitCoprod_symm_apply, coprodComm_symm_apply, Subgroup.subgroupOfContinuousMulEquivOfLe_apply, SpecialLinearGroup.centerEquivRootsOfUnity_apply, AffineEquiv.equivUnitsAffineMap_symm_apply_symm_apply, NumberField.IsCMField.unitsMulComplexConjInv_apply, toAdditive_symm_apply_apply, uliftPowersHom_apply_apply, multiplicativeAdditive_symm_apply, IsFreeGroup.toFreeGroup_apply, piUnique_apply, AddConstEquiv.equivUnits_symm_apply_apply, AlgEquiv.opComm_apply_symm_apply, coe_prodAssoc_symm, Subsemigroup.mem_map_equiv, Con.quotientKerEquivOfRightInverse_apply, CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_symm_apply_inv, ClassGroup.equivPic_symm_apply, CategoryTheory.Groupoid.vertexGroupIsomOfMap_symm_apply, SubMulAction.ofStabilizer.conjMap_comp, Subgroup.index_map_equiv, ConjAct.ofConjAct_toConjAct, RingEquiv.piCongrLeft_apply, AffineEquiv.equivUnitsAffineMap_symm_apply_toFun, SemimoduleCat.Iso.conj_eq_conj, associatesEquivOfUniqueUnits_apply, MulAction.zpowersQuotientStabilizerEquiv_symm_apply, toEquiv_ofLexMulEquiv, Abelianization.equivOfComm_apply, Submonoid.LocalizationMap.of_mulEquivOfMulEquiv_apply, NumberField.IsCMField.unitsComplexConj_eq_self_iff, HNNExtension.toSubgroupEquiv_neg_apply, SemidirectProduct.congr'_symm_apply_left, CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_π, symmEquiv_symm_apply_apply, Subsemigroup.map_equiv_eq_comap_symm, toMultiplicative_toAdditive_apply, GroupExtension.inl_conjAct_comm, Subring.centerCongr_symm_apply_coe, Equiv.Perm.OnCycleFactors.Subgroup.Centralizer.toConjAct_smul_mem_cycleFactorsFinset, ValuationSubring.principalUnitGroupEquiv_apply, AlgEquiv.autCongr_apply, galRestrict_apply, MulAut.conj_symm_apply, orderOf_eq, coe_monoidHom_trans, cast_apply, CategoryTheory.Iso.symm_self_conj, mulDissociated_preimage, MonoidHom.ofLeftInverse_apply, Matrix.SpecialLinearGroup.eq_scalar_center_equiv_rootsOfUnity, mkFactorOrderIsoOfFactorDvdEquiv_symm_apply_coe, Ideal.coe_smul_primesOver_eq_map_galRestrict, Submonoid.LocalizationMap.ofMulEquivOfLocalizations_apply, Submonoid.LocalizationMap.mulEquivOfLocalizations_left_inv_apply, DomMulAct.stabilizerMulEquiv_apply, MonoidHom.ker_comp_mulEquiv, WithZero.toMulBot_coe, coprodComm_apply, Subsemigroup.topEquiv_apply, Localization.mulEquivOfQuotient_monoidOf, FreeGroupBasis.lift_symm_apply, symmEquiv_symm_apply_symm_apply, toEquiv_symm, Submonoid.powLogEquiv_apply, MulEquivClass.coe_symm_apply_apply, piUnique_symm_apply, GroupExtension.Equiv.coe_toMulEquiv, Subgroup.conjAct_pointwise_smul_eq_self, Con.congr_mk, Localization.mulEquivOfQuotient_apply, ValuationSubring.coe_unitGroupMulEquiv_symm_apply, Submonoid.LocalizationMap.ofMulEquivOfDom_apply, AlgEquiv.val_inv_algHomUnitsEquiv_symm_apply, LinearOrderedCommGroupWithZero.fst_apply, MulEquivClass.apply_coe_symm_apply, opOp_apply, MulAut.congr_apply, Submonoid.leftInvEquiv_symm_eq_inv, ofLeftInverse'_symm_apply, Algebra.IsAlgebraic.algEquivEquivAlgHom_apply, IsCyclic.mulAutMulEquiv_symm_apply_symm_apply, toAdditive_symm_apply_symm_apply, galRestrictHom_symm_apply, monoidHomCongrRight_apply, punitCoprod_apply, CategoryTheory.Iso.self_symm_conj, Units.toAut_inv, Submonoid.LocalizationMap.ofMulEquivOfLocalizations_eq_iff_eq, MonoidAlgebra.mapDomainRingEquiv_apply, nonZeroDivisorsEquivUnits_apply, CategoryTheory.Iso.conjAut_hom, Submonoid.coe_equivMapOfInjective_apply, Equiv.Perm.equivUnitsEnd_symm_apply_symm_apply, Submonoid.LocalizationMap.mulEquivOfMulEquiv_mk', abelianizationCongr_of, SubMulAction.fixingSubgroupEquivFixingSubgroup_coe_apply, coe_toLexMulEquiv, Algebra.IsAlgebraic.algEquivEquivAlgHom_symm_apply, toUnits_symm_apply, Units.coe_opEquiv_symm, Equiv.permCongrHom_coe_equiv, Matrix.SpecialLinearGroup.toLin_equiv.toLinearMap_eq, MonoidHom.ofInjective_apply, coe_subgroupMap_apply, rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar_val, MulAutMultiplicative_apply_symm_apply, ModuleCat.Iso.conj_eq_conj, nonZeroDivisorsEquivUnits_symm_apply_coe, Equiv.Perm.cycleFactorsFinset_conj, toMulHom_eq_coe, WithZero.withZeroUnitsEquiv_symm_apply, CategoryTheory.Iso.conj_id, coprodCongr_symm_apply, PresentedGroup.equivPresentedGroup_symm_apply_of, CategoryTheory.ActionCategory.stabilizerIsoEnd_apply, comp_left_injective, SubMulAction.ofFixingSubgroup_of_eq_bijective, IsGaloisGroup.mulEquivAlgEquiv_symm_apply, CategoryTheory.Iso.trans_conj, funUnique_apply, Equiv.Perm.equivUnitsEnd_symm_apply_apply, rootsOfUnityCircleEquiv_apply, Action.resEquiv_inverse, toUnits_val_apply, SemidirectProduct.inv_left, coprodAssoc_symm_apply_inl, Subgroup.IsComplement'.QuotientMulEquiv_symm_apply, symm_comp_eq, MulOpposite.coe_opMulEquiv, uliftZPowersHom_apply_apply, Submonoid.comap_equiv_eq_map_symm, SemidirectProduct.mulEquivSubgroup_apply, Subsemigroup.map_equiv_top, IsCyclic.mulAutMulEquiv_symm_apply_apply, CoxeterSystem.map_simple, withZero_symm_apply_apply, op_symm_apply_symm_apply, CategoryTheory.Iso.conjAut_zpow, Subgroup.mem_iff_toUnits_mem_units, MulAut.conjNormal_inv_apply, Submonoid.map_equiv_top, bijective, Subgroup.subgroupOfEquivOfLe_apply_coe, SemidirectProduct.mulEquivProd_apply, ConjAct.ofConjAct_mul, mulEquivOfOrderOfEq_apply_gen, coe_toEquiv, QuotientGroup.quotientBot_apply, CoxeterMatrix.reindexGroupEquiv_symm_apply_simple, AffineEquiv.val_inv_equivUnitsAffineMap_apply, MonoidAlgebra.domCongr_support, Submonoid.leftInvEquiv_symm_fromLeftInv, autEquivRootsOfUnity_apply_rootOfSplit, SpecialLinearGroup.centerEquivRootsOfUnity_apply_apply, AddConstEquiv.equivUnits_symm_apply_symm_apply, SemidirectProduct.mulEquivSubgroup_symm_apply, freeGroupEquivCoprodI_apply, Unitary.conjStarAlgAut_symm_unitaryLinearIsometryEquiv, CategoryTheory.Functor.FullyFaithful.mulEquivEnd_apply, ConjAct.ofConjAct_inv, Action.resEquiv_functor, coe_toEquiv_symm, ClassGroup.equiv_mk0, WithZero.toMulBot_le, op_symm_apply_apply, Monoid.End_apply, SubMulAction.ofStabilizer.conjMap_bijective, Submonoid.LocalizationMap.mulEquivOfMulEquiv_eq, SemidirectProduct.mulEquivProd_symm_apply_right, Submonoid.LocalizationMap.symm_comp_ofMulEquivOfLocalizations_apply, MulAut.apply_inv_self, CategoryTheory.Iso.conj_comp, map_mul, Subgroup.equivSMul_symm_apply_coe, Subgroup.comap_normalClosure, coprodAssoc_symm_apply_inr_inl, Subgroup.IsComplement'.QuotientMulEquiv_apply, WithZero.withZeroUnitsEquiv_apply, HNNExtension.equiv_symm_eq_conj, FreeGroup.freeGroupCongr_apply, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_coe, Submonoid.topEquiv_toMonoidHom, Action.Iso.conj_ρ, ModularForm.coe_translate, piCongrRight_apply, SemidirectProduct.mul_left, FreeGroupBasis.map_apply, subsemigroupMap_apply_coe, subsemigroupMap_symm_apply_coe, subgroupMap_symm_apply, Nonneg.val_inv_unitsEquivPos_symm_apply_coe, val_rootsOfUnityEquivOfPrimitiveRoots_apply_coe, FreeMonoid.freeMonoidCongr_symm_of, coe_toMulHom, ClassGroup.equivPic_apply, Submonoid.val_unitsTypeEquivIsUnitSubmonoid_symm_apply, MonoidHom.toHomUnitsMulEquiv_symm_apply, AddOpposite.opMulEquiv_apply, val_piUnits_apply, coe_monoidHom_comp_coe_monoidHom_symm, Equiv.mulEquiv_symm_apply, Equiv.Perm.mem_conj_support, toSingleObjEquiv_functor_map, addMonoidEndToMultiplicative_apply_apply, ofBijective_apply, Subgroup.normalizerMonoidHom_apply_symm_apply_coe, galRestrictHom_apply, LinearOrderedCommGroupWithZero.inl_apply, Unitization.val_unitsFstOne_mulEquiv_quasiregular_apply, Con.comap_conGen_equiv, LinearOrderedCommGroupWithZero.inr_apply, coe_monoidHom_refl, Submonoid.centerCongr_apply_coe, CategoryTheory.Hom.mulEquivCongrRight_apply, Subgroup.centerToMulOpposite_symm_apply_coe, Localization.mulEquivOfQuotient_symm_mk', Submonoid.powLogEquiv_symm_apply, injective, ConjAct.toConjAct_ofConjAct, FGModuleCat.Iso.conj_hom_eq_conj, MonoidHom.apply_ofInjective_symm, powersMulHom_symm_apply, MulOpposite.opMulEquiv_symm_apply, Subsemigroup.coe_equivMapOfInjective_apply, QuotientGroup.quotientBot_symm_apply, Equiv.Perm.val_inv_equivUnitsEnd_apply, Submonoid.LocalizationMap.symm_comp_ofMulEquivOfLocalizations_apply', ConjAct.toConjAct_one, CategoryTheory.Iso.conjAut_pow, LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv, algebraMap_galRestrictHom_apply, SubMulAction.ofStabilizer.conjMap_apply, Subgroup.topEquiv_apply, symm_apply_apply, CategoryTheory.Iso.conj_apply, ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk, AddConstEquiv.coe_val_equivUnits_apply, WithZero.toMulBot_symm_bot, CategoryTheory.PreGaloisCategory.endMulEquivAutGalois_pi, rootsOfUnityEquivOfPrimitiveRoots_symm_apply, Units.mapContinuousMulEquiv_apply, MonoidAlgebra.domCongr_apply, StarMulEquiv.coe_toMulEquiv, ValuationSubring.coe_unitGroupToResidueFieldUnits_apply, AddAutAdditive_symm_apply_apply, SubMulAction.ofFixingSubgroup_insert_map_bijective, PresentedGroup.equivPresentedGroup_apply_of, AddAut.congr_apply, ConjAct.ofConjAct_one, Subgroup.map_equiv_eq_comap_symm, Subgroup.IsArithmetic.conj, subgroupCongr_symm_apply, Submonoid.topEquiv_apply, CategoryTheory.ActionCategory.stabilizerIsoEnd_symm_apply, lipschitzGroup.conjAct_smul_range_ι, WithZero.toMulBot_strictMono, SubMulAction.conjMap_ofFixingSubgroup_bijective, Units.coe_mapEquiv, AffineEquiv.equivUnitsAffineMap_symm_apply_invFun, IsGaloisGroup.map_mulEquivAlgEquiv_fixingSubgroup, IsCyclotomicExtension.autEquivPow_symm_apply, WithZero.unitsWithZeroEquiv_apply, AlgEquiv.algHomUnitsEquiv_apply_apply, IsCusp.smul, Rat.ringOfIntegersWithValEquiv_apply, SpecialLinearGroup.centerEquivRootsOfUnity_apply_of_finrank_le_one, map_finprod_mem, ClassGroup.equiv_mk, symmEquiv_apply_symm_apply, ConjAct.smul_eq_mulAut_conj, addMonoidEndToMultiplicative_symm_apply_apply, Matrix.GeneralLinearGroup.toLin_apply, AddEquiv.toMultiplicativeLeft_apply_apply, Subsemigroup.centerCongr_apply_coe, Subsemigroup.comap_equiv_eq_map_symm, ValuationSubring.principalUnitGroup_symm_apply, WithZero.withZeroUnitsEquiv_strictMono, MonoidHom.toMulEquiv_apply, RootPairing.Equiv.toEndUnit_val, coe_prodComm, Submonoid.LocalizationMap.mulEquivOfMulEquiv_eq_map_apply, Abelianization.equivOfComm_symm_apply, IsCyclotomicExtension.autEquivPow_apply, refl_apply, SubMulAction.conjMap_ofFixingSubgroup_coe_apply, val_inv_piUnits_symm_apply, Submodule.unitsQuotEquivRelPic_apply_coe, MonoidHom.toHomUnitsMulEquiv_apply, apply_symm_apply, QuotientGroup.quotientMulEquivOfEq_mk, CategoryTheory.Iso.commGroupIsoToMulEquiv_apply, IsCyclotomicExtension.Rat.galEquivZMod_smul_of_pow_eq, AddAut.congr_symm_apply, withZero_symm_apply_symm_apply, MulAut.congr_symm_apply, GrpWithZero.Iso.mk_inv, CategoryTheory.Iso.conjAut_trans, piMultiplicative_symm_apply, Submonoid.mul_leftInvEquiv_symm, prod_galRestrict_eq_norm, Subgroup.isCoatom_comap, autEquivRootsOfUnity_smul, inv_apply, MulAut.conjNormal_apply, unitary.linearIsometryEquiv_coe_apply
instInhabited 📖	CompOp	—
mk' 📖	CompOp	—
ofBijective 📖	CompOp	2 math math: ofBijective_apply_symm_apply, ofBijective_apply
refl 📖	CompOp	29 math math: monoidHomCongrLeftEquiv_refl, LinearMap.GeneralLinearGroup.congrLinearEquiv_refl, piCongrRight_refl, coe_refl, FreeGroup.freeGroupCongr_refl, monoidHomCongrRight_refl, Submonoid.LocalizationMap.ofMulEquivOfDom_id, symm_trans_self, Submonoid.LocalizationMap.ofMulEquivOfLocalizations_id, refl_symm, SkewMonoidAlgebra.domCongr_refl, AlgEquiv.autCongr_refl, monoidHomCongrLeft_refl, Submodule.unitsQuotEquivRelPic_symm_apply, ClassGroup.equivPic_symm_apply, abelianizationCongr_refl, MulAction.stabilizerEquivStabilizer_one, self_trans_symm, SpecialLinearGroup.congr_linearEquiv_refl, QuotientGroup.equivQuotientZPowOfEquiv_refl, ClassGroup.equivPic_apply, coe_monoidHom_refl, monoidHomCongrRightEquiv_refl, withOneCongr_refl, MulAut.one_def, MonoidAlgebra.domCongr_refl, RingEquiv.coe_mulEquiv_refl, refl_apply, Submodule.unitsQuotEquivRelPic_apply_coe
symmEquiv 📖	CompOp	4 math math: symmEquiv_apply_apply, symmEquiv_symm_apply_apply, symmEquiv_symm_apply_symm_apply, symmEquiv_apply_symm_apply
toEquiv 📖	CompOp	19 math math: RingEquiv.toEquiv_commutes, OrderMonoidIso.invFun_eq_symm, map_mul', invFun_eq_symm, ContinuousMulEquiv.continuous_toFun, OrderMonoidIso.map_le_map_iff', ContinuousMulEquiv.invFun_eq_symm, ContinuousMulEquiv.continuous_invFun, toHomeomorph_toContinuousMulEquiv, toFun_eq_coe, toEquiv_eq_coe, StarMulEquiv.map_star', symm_map_mul, submonoidMap_symm_apply, OrderMonoidIso.toFun_eq_coe, toEquiv_injective, Equiv.Perm.cycleFactorsFinset_conj, subgroupMap_symm_apply, ContinuousMulEquiv.toEquiv_eq_coe
toMonoidHom 📖	CompOp	66 math math: CommGrpCat.uliftFunctor_map, Submonoid.mem_map_equiv, toCommMonCatIso_hom, SubMulAction.fixingSubgroup_smul_eq_fixingSubgroup_map_conj, FDRep.endRingEquiv_symm_comp_ρ, Subgroup.Characteristic.fixed, toAdditive_apply_apply, Subgroup.comap_toSubmonoid, Subgroup.comap_equiv_eq_map_symm', toMonoidHom_eq_coe, Submonoid.LocalizationMap.ofMulEquivOfLocalizations_comp, Monoid.CoprodI.inv_def, monoidHomCongrLeftEquiv_apply, Subgroup.characteristic_iff_comap_eq, Subgroup.mem_map_equiv, toSingleObjEquiv_unitIso_hom, Subgroup.characteristic_iff_comap_le, Subgroup.characteristic_iff_map_le, coe_comapSubgroup, MulAction.stabilizer_smul_eq_stabilizer_map_conj, MulAction.IsBlock.of_subgroup_of_conjugate, toSingleObjEquiv_counitIso_hom, coe_toMonoidHom, coe_mapSubgroup, toMonCatIso_inv, AddEquiv.toMultiplicativeLeft_symm_apply_symm_apply, toCommGrpIso_inv, Subgroup.characteristic_iff_le_comap, Subgroup.exists_mulEquiv_eq_graph, AddEquiv.toMultiplicativeRight_symm_apply_apply, toSingleObjEquiv_unitIso_inv, monoidHomCongrRightEquiv_apply, toSingleObjEquiv_counitIso_inv, toMonCatIso_hom, AddEquiv.toMultiplicativeRight_symm_apply_symm_apply, RingEquiv.toMonoidHom_commutes, AddEquiv.toMultiplicative_symm_apply_apply, MonCat.uliftFunctor_map, Subgroup.goursat_surjective, toMonoidHom_injective, SubMulAction.fixingSubgroup_map_conj_eq, AddEquiv.toMultiplicative_symm_apply_symm_apply, Subgroup.map_equiv_eq_comap_symm', ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply, toGrpIso_inv, toAdditive_apply_symm_apply, toCommMonCatIso_inv, toCommGrpIso_hom, CommMonCat.uliftFunctor_map, Submonoid.exists_mulEquiv_eq_mgraph, FDRep.of_ρ, AddEquiv.toMultiplicativeLeft_symm_apply_apply, Subgroup.characteristic_iff_map_eq, toGrpIso_hom, Submonoid.divPairs_comap, GrpCat.uliftFunctor_map, monoidHomCongrRightEquiv_symm_apply, MonoidHom.exists_mulEquiv_range_eq_graph, Submonoid.LocalizationMap.ofMulEquivOfLocalizations_eq, monoidHomCongrLeftEquiv_symm_apply, Subgroup.goursat, FDRep.endRingEquiv_comp_ρ, Subgroup.characteristic_iff_le_map, Subgroup.map_equiv_normalizer_eq, MonoidHom.exists_mulEquiv_mrange_eq_mgraph, Subgroup.centralizer_eq_comap_stabilizer
toMulHom 📖	CompOp	7 math math: withOneCongr_apply, toMagmaCatIso_hom, toSemigrpIso_inv, toMagmaCatIso_inv, toMulHom_eq_coe, toSemigrpIso_hom, coe_toMulHom
trans 📖	CompOp	32 math math: abelianizationCongr_trans, coe_trans, CoxeterSystem.reindex_mulEquiv, FreeGroup.freeGroupCongr_trans, MonoidAlgebra.mapDomainRingEquiv_trans, MulAction.stabilizerEquivStabilizer_trans, Submonoid.LocalizationMap.ofMulEquivOfLocalizations_comp, StarMulEquiv.toMulEquiv_trans, SpecialLinearGroup.centerCongr_toLin_equiv_trans_centerEquivRootsOfUnity_eq, symm_trans_self, monoidHomCongrLeft_trans, piCongrRight_trans, RingEquiv.coe_mulEquiv_trans, trans_apply, withOneCongr_trans, MulAut.mul_def, symm_trans_apply, monoidHomCongrRight_trans, CoxeterSystem.map_mulEquiv, coe_monoidHom_trans, QuotientGroup.equivQuotientZPowOfEquiv_trans, monoidHomCongrLeftEquiv_trans, MulAut.congr_apply, LinearMap.GeneralLinearGroup.congrLinearEquiv_trans', self_trans_symm, LinearMap.GeneralLinearGroup.congrLinearEquiv_trans, monoidHomCongrRightEquiv_trans, SpecialLinearGroup.congr_linearEquiv_trans, Equiv.permCongrHom_trans, AlgEquiv.autCongr_trans, OrderMonoidIso.coe_trans_mulEquiv, MulAut.congr_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eq_iff_eq 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike	—	injective
apply_eq_iff_symm_apply 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.apply_eq_iff_eq_symm_apply
apply_symm_apply 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.apply_symm_apply
bijective 📖	mathematical	—	Function.Bijective DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike	—	EquivLike.bijective
cast_apply 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike cast	—	—
cast_symm_apply 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike symm cast	—	—
coe_mk 📖	mathematical	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	MulEquiv instEquivLike	—	—
coe_monoidHom_comp_coe_monoidHom_symm 📖	mathematical	—	MonoidHom.comp MulOneClass.toMulOne MonoidHomClass.toMonoidHom MulEquiv MulOne.toMul EquivLike.toFunLike instEquivLike MulEquivClass.instMonoidHomClass instMulEquivClass symm MonoidHom.id	—	MonoidHom.ext MulEquivClass.instMonoidHomClass instMulEquivClass apply_symm_apply
coe_monoidHom_refl 📖	mathematical	—	MonoidHomClass.toMonoidHom MulEquiv MulOne.toMul MulOneClass.toMulOne EquivLike.toFunLike instEquivLike MulEquivClass.instMonoidHomClass instMulEquivClass refl MonoidHom.id	—	MulEquivClass.instMonoidHomClass instMulEquivClass
coe_monoidHom_symm_comp_coe_monoidHom 📖	mathematical	—	MonoidHom.comp MulOneClass.toMulOne MonoidHomClass.toMonoidHom MulEquiv MulOne.toMul EquivLike.toFunLike instEquivLike MulEquivClass.instMonoidHomClass instMulEquivClass symm MonoidHom.id	—	MonoidHom.ext MulEquivClass.instMonoidHomClass instMulEquivClass symm_apply_apply
coe_monoidHom_trans 📖	mathematical	—	MonoidHomClass.toMonoidHom MulEquiv MulOne.toMul MulOneClass.toMulOne EquivLike.toFunLike instEquivLike MulEquivClass.instMonoidHomClass instMulEquivClass trans MonoidHom.comp	—	MulEquivClass.instMonoidHomClass instMulEquivClass
coe_refl 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike refl	—	—
coe_toEquiv 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike EquivLike.toEquiv MulEquiv instEquivLike	—	—
coe_toEquiv_symm 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm EquivLike.toEquiv MulEquiv instEquivLike symm	—	—
coe_toMonoidHom 📖	mathematical	—	DFunLike.coe MonoidHom MulOneClass.toMulOne MonoidHom.instFunLike toMonoidHom MulEquiv MulOne.toMul EquivLike.toFunLike instEquivLike	—	—
coe_toMulHom 📖	mathematical	—	DFunLike.coe MulHom MulHom.funLike toMulHom MulEquiv EquivLike.toFunLike instEquivLike	—	—
coe_trans 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike trans	—	—
comp_left_injective 📖	mathematical	—	MonoidHom MulOneClass.toMulOne MonoidHom.comp MonoidHomClass.toMonoidHom MulEquiv MulOne.toMul EquivLike.toFunLike instEquivLike MulEquivClass.instMonoidHomClass instMulEquivClass	—	MulEquivClass.instMonoidHomClass instMulEquivClass coe_monoidHom_comp_coe_monoidHom_symm MonoidHom.comp_id
comp_right_injective 📖	mathematical	—	MonoidHom MulOneClass.toMulOne MonoidHom.comp MonoidHomClass.toMonoidHom MulEquiv MulOne.toMul EquivLike.toFunLike instEquivLike MulEquivClass.instMonoidHomClass instMulEquivClass	—	MulEquivClass.instMonoidHomClass instMulEquivClass coe_monoidHom_symm_comp_coe_monoidHom MonoidHom.id_comp
comp_symm_eq 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.comp_symm_eq
congr_arg 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike	—	DFunLike.congr_arg
congr_fun 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike	—	DFunLike.congr_fun
eq_comp_symm 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.eq_comp_symm
eq_symm_apply 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.eq_symm_apply
eq_symm_comp 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.eq_symm_comp
equivLike_inv_eq_symm 📖	mathematical	—	EquivLike.inv MulEquiv instEquivLike DFunLike.coe EquivLike.toFunLike symm	—	—
ext 📖	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike	—	ext
injective 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike	—	EquivLike.injective
instMulEquivClass 📖	mathematical	—	MulEquivClass MulEquiv instEquivLike	—	map_mul'
invFun_eq_symm 📖	mathematical	—	Equiv.invFun toEquiv DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike symm	—	—
map_div 📖	mathematical	—	DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid DivisionMonoid.toDivInvMonoid EquivLike.toFunLike instEquivLike DivInvMonoid.toDiv	—	map_div MulEquivClass.instMonoidHomClass instMulEquivClass
map_eq_one_iff 📖	mathematical	—	DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne EquivLike.toFunLike instEquivLike MulOne.toOne	—	EmbeddingLike.map_eq_one_iff EquivLike.toEmbeddingLike MonoidHomClass.toOneHomClass MulEquivClass.instMonoidHomClass instMulEquivClass
map_inv 📖	mathematical	—	DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid DivisionMonoid.toDivInvMonoid EquivLike.toFunLike instEquivLike DivInvMonoid.toInv	—	map_inv MulEquivClass.instMonoidHomClass instMulEquivClass
map_mul 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike	—	map_mul MulEquivClass.instMulHomClass instMulEquivClass
map_mul' 📖	mathematical	—	Equiv.toFun toEquiv	—	—
map_ne_one_iff 📖	—	—	—	—	EmbeddingLike.map_ne_one_iff EquivLike.toEmbeddingLike MonoidHomClass.toOneHomClass MulEquivClass.instMonoidHomClass instMulEquivClass
map_one 📖	mathematical	—	DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne EquivLike.toFunLike instEquivLike MulOne.toOne	—	map_one MonoidHomClass.toOneHomClass MulEquivClass.instMonoidHomClass instMulEquivClass
mk_coe 📖	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike Equiv.toFun	—	—	ext
mk_coe' 📖	mathematical	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike Equiv.toFun	symm	—	Function.Bijective.injective symm_bijective ext
ofBijective_apply 📖	mathematical	Function.Bijective DFunLike.coe	MulEquiv EquivLike.toFunLike instEquivLike ofBijective	—	—
ofBijective_apply_symm_apply 📖	mathematical	Function.Bijective DFunLike.coe MonoidHom MulOneClass.toMulOne MonoidHom.instFunLike	MulEquiv MulOne.toMul EquivLike.toFunLike instEquivLike symm ofBijective MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass	—	apply_symm_apply MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass
refl_apply 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike refl	—	—
refl_symm 📖	mathematical	—	symm refl	—	—
self_comp_symm 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike symm	—	apply_symm_apply
self_trans_symm 📖	mathematical	—	trans symm refl	—	DFunLike.ext symm_apply_apply
surjective 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike	—	EquivLike.surjective
symmEquiv_apply_apply 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike Equiv Equiv.instEquivLike symmEquiv symm	—	—
symmEquiv_apply_symm_apply 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike symm Equiv Equiv.instEquivLike symmEquiv	—	—
symmEquiv_symm_apply_apply 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike Equiv Equiv.instEquivLike Equiv.symm symmEquiv symm	—	—
symmEquiv_symm_apply_symm_apply 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike symm Equiv Equiv.instEquivLike Equiv.symm symmEquiv	—	—
symm_apply_apply 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.symm_apply_apply
symm_apply_eq 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.symm_apply_eq
symm_bijective 📖	mathematical	—	Function.Bijective MulEquiv symm	—	Function.bijective_iff_has_inverse symm_symm
symm_comp_eq 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.symm_comp_eq
symm_comp_self 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike symm	—	symm_apply_apply
symm_map_mul 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm toEquiv	—	map_mul MulHom.mulHomClass Equiv.left_inv Equiv.right_inv
symm_mk 📖	mathematical	Equiv.toFun	symm Equiv.symm symm_map_mul	—	—
symm_symm 📖	mathematical	—	symm	—	—
symm_trans_apply 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike symm trans	—	—
symm_trans_self 📖	mathematical	—	trans symm refl	—	DFunLike.ext apply_symm_apply
toEquiv_eq_coe 📖	mathematical	—	toEquiv EquivLike.toEquiv MulEquiv instEquivLike	—	—
toEquiv_injective 📖	mathematical	—	MulEquiv Equiv toEquiv	—	—
toEquiv_symm 📖	mathematical	—	EquivLike.toEquiv MulEquiv instEquivLike symm Equiv.symm	—	—
toFun_eq_coe 📖	mathematical	—	Equiv.toFun toEquiv DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike	—	—
toMonoidHom_eq_coe 📖	mathematical	—	toMonoidHom MonoidHomClass.toMonoidHom MulEquiv MulOne.toMul MulOneClass.toMulOne EquivLike.toFunLike instEquivLike MulEquivClass.instMonoidHomClass instMulEquivClass	—	—
toMonoidHom_injective 📖	mathematical	—	MulEquiv MulOne.toMul MulOneClass.toMulOne MonoidHom toMonoidHom	—	Function.Injective.of_comp DFunLike.coe_injective
toMulHom_eq_coe 📖	mathematical	—	toMulHom MulHomClass.toMulHom MulEquiv EquivLike.toFunLike instEquivLike MulEquivClass.instMulHomClass instMulEquivClass	—	—
trans_apply 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike instEquivLike trans	—	—

MulEquiv.Simps

Definitions

Name	Category	Theorems
symm_apply 📖	CompOp	—

MulEquivClass

Definitions

Name	Category	Theorems
toMulEquiv 📖	CompOp	42 math math: Subgroup.subgroupOfContinuousMulEquivOfLe_toMulEquiv, RingEquiv.toEquiv_commutes, OrderMonoidIso.withZero_symm_apply_symm_apply, OrderMonoidIso.withZero_symm_apply_apply, OrderMonoidIso.val_unitsCongr_symm_apply, MulEquiv.toMulEquiv_toContinuousMulEquiv, map_dvd_iff_dvd_symm, NonUnitalSubsemiring.centerCongr_symm_apply_coe, Subsemiring.centerCongr_symm_apply_coe, GroupExtension.Equiv.toMulEquiv_eq_coe, RingEquiv.coe_toMulEquiv, Submonoid.map_coe_toMulEquiv, OrderMonoidIso.coe_mulEquiv, OrderMonoidIso.val_inv_unitsCongr_symm_apply, GroupExtension.Equiv.coe_symm, AlgEquiv.symm_toMulEquiv, OrderMonoidIso.withZero_apply_symm_apply, UniqueFactorizationMonoid.normalizedFactorsEquiv_symm_apply, OrderMonoidIso.toMulEquiv_eq_coe, NonUnitalSubring.centerCongr_symm_apply_coe, RingEquiv.coe_mulEquiv_trans, OrderMonoidIso.withZero_apply_apply, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply, NumberField.RingOfIntegers.withValEquiv_apply, ContinuousMulEquiv.toMulEquiv_eq_coe, RingEquiv.toMonoidHom_commutes, RingEquiv.prodProdProdComm_toMulEquiv, AlgEquiv.opComm_apply_symm_apply, RingEquiv.piCongrLeft_apply, Subring.centerCongr_symm_apply_coe, Units.toMulEquiv_mapContinuousMulEquiv, coe_symm_apply_apply, GroupExtension.Equiv.coe_toMulEquiv, apply_coe_symm_apply, RingEquiv.toMulEquiv_eq_coe, toMulEquiv_injective, RingEquiv.coe_toMulEquiv_symm, Units.mapContinuousMulEquiv_apply, Rat.ringOfIntegersWithValEquiv_apply, ClassGroup.equiv_mk, RingEquiv.coe_mulEquiv_refl, OrderMonoidIso.coe_trans_mulEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_coe_symm_apply 📖	mathematical	—	DFunLike.coe EquivLike.toFunLike MulEquiv MulEquiv.instEquivLike MulEquiv.symm toMulEquiv	—	Equiv.right_inv
coe_symm_apply_apply 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm toMulEquiv	—	Equiv.left_inv
instMonoidHomClass 📖	mathematical	—	MonoidHomClass MulOneClass.toMulOne EquivLike.toFunLike	—	instMulHomClass mul_one EquivLike.right_inv map_mul one_mul
instMulHomClass 📖	mathematical	—	MulHomClass EquivLike.toFunLike	—	map_mul
map_eq_one_iff 📖	mathematical	—	DFunLike.coe	—	EmbeddingLike.map_eq_one_iff
map_mul 📖	mathematical	—	DFunLike.coe EquivLike.toFunLike	—	—
map_ne_one_iff 📖	—	—	—	—	EmbeddingLike.map_ne_one_iff

MulHom

Definitions

Name	Category	Theorems
toMulEquiv 📖	CompOp	2 math math: toMulEquiv_symm_apply, toMulEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toMulEquiv_apply 📖	mathematical	comp id	DFunLike.coe MulEquiv EquivLike.toFunLike MulEquiv.instEquivLike toMulEquiv MulHom funLike	—	—
toMulEquiv_symm_apply 📖	mathematical	comp id	DFunLike.coe MulEquiv EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm toMulEquiv MulHom funLike	—	—

(root)

Definitions

Name	Category	Theorems
AddEquiv 📖	CompData	673 math math: val_toAddUnits_apply, AddSubgroup.centerToAddOpposite_apply_coe, OrderAddMonoidIso.toAddEquiv_injective, DFinsupp.liftAddHom_apply, CochainComplex.HomComplex.Cochain.rightShiftAddEquiv_symm_apply, AddEquiv.coprodComm_apply, AddMonoidAlgebra.mapDomainRingEquiv_apply, AddEquiv.ofLeftInverse'_apply, ContinuousMap.addEquivBoundedOfCompact_apply, AddMonoidAlgebra.domCongr_comp_lsingle, AddSubmonoid.LocalizationMap.symm_comp_ofAddEquivOfLocalizations_apply, WithConv.addEquiv_symm_apply_ofConv, AddSubmonoid.LocalizationMap.addEquivOfAddEquiv_eq, CochainComplex.HomComplex.Cocycle.leftShiftAddEquiv_symm_apply, MonomialOrder.degree_add_of_ne, AddEquiv.toMultiplicative_apply_symm_apply, Multiset.toFinsupp_add, AddAut.apply_inv_self, Rep.diagonalSuccIsoFree_inv_hom_single, CochainComplex.HomComplex.Cocycle.equivHom_symm_apply, AddEquiv.addSubgroupMap_symm_apply, Int.card_fintype_addEquiv, AddEquiv.piAdditive_apply, Multiset.equivDFinsupp_symm_apply, DFinsupp.liftAddHom_apply_single, WithLp.addEquiv_apply, AddEquiv.toAddMonoidHom_eq_coe, AddAutAdditive_apply_symm_apply, Complex.equivRealProdAddHom_symm_apply, Rep.leftRegularHom_hom, AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid_apply_coe, AddMonoidHom.ker_comp_addEquiv, AddEquiv.invFun_eq_symm, AddSubgroup.index_map_equiv, AddMonoidHom.toAddEquiv_symm_apply, Subring.addEquivOp_apply_coe, AddEquiv.prodUnique_apply, CochainComplex.HomComplex.Cochain.fromSingleEquiv_fromSingleMk, WithConv.toEquiv_addEquiv, Matrix.entryAddHom_eq_comp, AddSubgroup.addSubgroupOfContinuousAddEquivOfLe_apply, Finsupp.sumFinsuppAddEquivProdFinsupp_symm_inl, AddMonoidAlgebra.mapRangeAddEquiv_apply, AddEquiv.coprodPUnit_symm_apply, HahnSeries.addOppositeEquiv_symm_support, AddAut.mulRight_symm_apply, MulEquiv.toAdditive_apply_apply, AddMonoidAlgebra.mapDomainAddEquiv_single, CategoryTheory.Abelian.Ext.mk₀_addEquiv₀_apply, AddEquiv.toMultiplicativeRight_apply_apply, SubAddAction.ofStabilizer.conjMap_comp, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_left, AddAut.mul_apply, AddEquiv.additiveMultiplicative_apply, sigmaFinsuppAddEquivDFinsupp_apply, AddSubmonoid.fromLeftNeg_leftNegEquiv_symm, AddEquiv.neg_apply, MulOpposite.opAddEquiv_apply, AddSubgroup.comap_equiv_eq_map_symm, AddMonoidAlgebra.domCongr_toAlgHom, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_postcomp, AddSubmonoid.val_neg_addUnitsTypeEquivIsAddUnitAddSubmonoid_symm_apply, AddCommGroup.equiv_directSum_zmod_of_finite', AddMonoidAlgebra.mapDomainAddEquiv_apply, MultilinearMap.domDomCongrEquiv_symm_apply, AddSubmonoid.LocalizationMap.addEquivOfLocalizations_symm_apply, MonomialOrder.degree_sub_le, Finsupp.sigmaFinsuppAddEquivPiFinsupp_apply, AddEquivClass.apply_coe_symm_apply, AddSubmonoid.add_leftNegEquiv_symm, AddEquiv.map_zero, multiplesAddHom_apply, AddEquiv.val_neg_piAddUnits_apply, uliftMultiplesHom_symm_apply, AddEquiv.funUnique_symm_apply, AddHom.toAddEquiv_apply, AddEquiv.coe_prodComm_symm, AddEquiv.symm_comp_eq, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_right, AddHom.toAddEquiv_symm_apply, AddSubmonoid.coe_equivMapOfInjective_apply, AddMonoidAlgebra.toRingHom_mapDomainRingEquiv, AddEquiv.addSubgroupCongr_apply, Set.conj_mem_fixingAddSubgroup, AddEquiv.piUnique_apply, Matrix.uniqueAddEquiv_apply, RingEquiv.op_apply_symm_apply, AddAutAdditive_apply_apply, AddSubmonoid.LocalizationMap.addEquivOfAddEquiv_mk', Finsupp.toMultiset_toFinsupp, AddEquivClass.coe_symm_apply_apply, Finsupp.mapRange.addEquiv_apply, AddAutAdditive_symm_apply_symm_apply, MonomialOrder.degree_reduce_lt, AddOpposite.opAddEquiv_apply, Finsupp.llift_apply, QuotientAddGroup.liftEquiv_coe, AddSubmonoid.LocalizationMap.ofAddEquivOfLocalizations_eq_iff_eq, AddSubsemigroup.mem_map_equiv, AddEquiv.comp_symm_eq, Int.univ_addEquiv, Multiset.toFinsupp_sum_eq, AddMonoidHom.apply_ofInjective_symm, Finsupp.sumFinsuppAddEquivProdFinsupp_symm_apply, AddUnits.coe_unop_opEquiv, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, MulAutMultiplicative_symm_apply_apply, AddSubgroup.mem_iff_toAddUnits_mem_addUnits, sigmaFinsuppAddEquivDFinsupp_symm_apply, AddMagmaCat.addEquiv_coe_eq, zmultiplesAddHom_symm_apply, AddEquiv.finsuppUnique_symm, AddEquiv.coe_addMonoidHom_refl, Representation.smul_ofModule_asModule, MonomialOrder.toSyn_strictMono, CochainComplex.HomComplex.Cocycle.equivHomShift'_symm_apply, WeierstrassCurve.Projective.Point.toAffineAddEquiv_apply, MonomialOrder.div_single, Subsemiring.addEquivOp_apply_coe, Finsupp.liftAddHom_comp_single, MonoidAlgebra.mapDomainAddEquiv_single, multiplesAddHom_symm_apply, AddSubmonoid.centerCongr_symm_apply_coe, SubAddAction.ofStabilizer.conjMap_comp_neg_apply, AddSubgroup.coe_equivMapOfInjective_apply, AddEquiv.symmEquiv_symm_apply_symm_apply, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, MulAutMultiplicative_apply_apply, Finsupp.mapRange.addEquiv_toEquiv, AddEquiv.withZeroCongr_apply, Matrix.coe_ofAddEquiv_symm, MonomialOrder.degree_add_le, AddSubsemigroup.topEquiv_apply, AddEquiv.prodProdProdComm_apply, AddEquiv.toMultiplicativeLeft_apply_symm_apply, AddEquiv.coe_addMonoidHom_comp_coe_addMonoidHom_symm, Multiset.equivDFinsupp_apply, AddEquiv.self_comp_symm, CochainComplex.HomComplex.CohomologyClass.toSmallShiftedHom_mk, addEquivOfAddOrderOfEq_apply_gen, Matrix.uniqueAddEquiv_symm_apply, HahnSeries.addOppositeEquiv_support, AddSubmonoid.centerToAddOpposite_symm_apply_coe, AddMonoidHom.ofLeftInverse_symm_apply, Subalgebra.mopAlgEquivOp_symm_apply, AddSubsemigroup.centerToAddOpposite_symm_apply_coe, DFinsupp.mapRange.addEquiv_apply, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_symm_apply, AddSemigrp.addEquiv_coe_eq, AddAut.conj_symm_apply, AddEquiv.toMultiplicativeRight_apply_symm_apply, Matrix.entryAddMonoidHom_eq_comp, AddEquiv.uniqueProd_symm_apply, MonomialOrder.le_degree, SubAddAction.conjMap_ofFixingAddSubgroup_bijective, CategoryTheory.Adjunction.compPreadditiveYonedaIso_inv_app_app_apply, AddSubsemigroup.comap_equiv_eq_map_symm, AddEquiv.map_dfinsuppSumAddHom, FreeAbelianGroup.liftAddEquiv_symm_apply, AddSubmonoid.LocalizationMap.of_addEquivOfAddEquiv_apply, AddEquiv.addMonoidHomCongrLeft_apply, LinearEquiv.funUnique_symm_apply, AddSubmonoid.LocalizationMap.symm_comp_ofAddEquivOfLocalizations_apply', AddSubgroup.mem_ofAddUnits_iff_toAddUnits_mem, AddEquiv.symm_apply_apply, QuotientAddGroup.liftEquiv_mk, AddSubgroup.addSubgroupOfEquivOfLe_apply_coe, AddAut.coe_inv, SubAddAction.conjMap_ofFixingAddSubgroup_coe_apply, Multiset.toFinsupp_union, AddEquiv.toAdditive_toMultiplicative_symm_apply, AlgEquiv.op_apply_symm_apply, AddSubmonoid.leftNegEquiv_add, Unitization.cobounded_eq_aux, DirectSum.addEquivProdDirectSum_symm_apply_toFun, CategoryTheory.Iso.addCommGroupIsoToAddEquiv_symm_apply, AddEquiv.map_eq_zero_iff, coe_addEquiv_lpPiLp_symm, MonomialOrder.lex_lt_iff_of_unique, SkewMonoidAlgebra.toFinsuppAddEquiv_apply, MulAutMultiplicative_symm_apply_symm_apply, FreeAbelianGroup.equivFinsupp_symm_apply, ModuleCat.homAddEquiv_symm_apply_hom, AddSubmonoid.map_equiv_top, AddCommGroup.equiv_free_prod_directSum_zmod, MonomialOrder.degLex_le_iff, AddEquiv.coe_prodAssoc, AddEquiv.coprodAssoc_apply_inr, AddSubmonoid.LocalizationMap.addEquivOfAddEquiv_eq_map_apply, Int.addSubgroup_index_ne_zero_iff, Finsupp.comp_liftAddHom, AddEquiv.piUnique_symm_apply, AddEquiv.funUnique_apply, SubAddAction.ofFixingAddSubgroup_of_eq_bijective, AddEquiv.coe_addSubmonoidMap_apply, AddEquiv.comp_left_injective, AddCommGrpCat.homAddEquiv_symm_apply_hom, AddEquiv.ofLeftInverse_apply, Multiset.toFinsupp_inter, MonomialOrder.degree_le_iff, AddMonoidAlgebra.domCongr_single, CategoryTheory.ProjectiveResolution.extMk_hom, AddSubsemigroup.topEquiv_symm_apply_coe, AddEquiv.op_symm_apply_symm_apply, Finsupp.domCongr_apply, Rep.toAdditive_symm_apply, AddAut.coe_mul, AddSubgroup.centerCongr_apply_coe, OrderAddMonoidIso.coe_addEquiv, Finsupp.lift_apply, AddSubmonoid.comap_equiv_eq_map_symm, AddEquiv.subsemigroupMap_apply_coe, CochainComplex.HomComplex.Cochain.leftShiftAddEquiv_apply, Multiset.toFinsupp_apply, exists_prime_addEquiv_ZMod, AddEquiv.neg'_apply, AddCircle.equivAddCircle_apply_mk, CochainComplex.HomComplex.Cochain.rightShiftAddEquiv_apply, OrderAddMonoidIso.coe_mk, AddEquiv.finsuppUnique_apply, AddSubsemigroup.centerCongr_apply_coe, AddAction.zmultiplesQuotientStabilizerEquiv_symm_apply, AddSubgroup.map_equiv_eq_comap_symm, AddCommGroup.equiv_directSum_zmod_of_finite, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, Finset.mapRange_finsuppAntidiag_eq, Rep.indResAdjunction_counit_app_hom_hom, QuaternionAlgebra.coe_addEquivProd, RingEquiv.coe_toAddEquiv, AddAction.stabilizerEquivStabilizer_symm_apply, AddCon.comap_conGen_equiv, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_pow', AddEquiv.toEquiv_symm, AddEquiv.prodProdProdComm_toEquiv, QuadraticForm.dualProdIsometry_invFun, AddEquiv.entryAddHom_comp_mapMatrix, MonomialOrder.degree_sum_le, AddCon.comapQuotientEquivOfSurj_symm_mk, AddLocalization.addEquivOfQuotient_mk', AddEquiv.symmEquiv_apply_symm_apply, Finite.exists_type_univ_nonempty_addEquiv, Subring.mopRingEquivOp_symm_apply, AddEquiv.map_finsum_mem, AddMonoid.IsTorsion.torsionAddEquiv_symm_apply_coe, AddEquiv.add_submonoid_map_symm_apply, AddSubmonoid.map_coe_toAddEquiv, AddSubmonoid.val_addUnitsTypeEquivIsAddUnitAddSubmonoid_symm_apply, Finsupp.snd_sumFinsuppAddEquivProdFinsupp, AddEquiv.mapAddSubgroup_symm_apply, Complex.equivRealProdAddHom_symm_apply_re, AddEquiv.arrowCongr_apply, Equiv.addEquiv_apply, AddEquiv.coprodPUnit_apply, AddMonoidHom.ofLeftInverse_apply, Complex.equivRealProdAddHom_symm_apply_im, Subsemiring.addEquivOp_symm_apply_coe, MonomialOrder.degree_mul_lt_iff_left_lt_of_ne_zero, Finsupp.coe_curryAddEquiv, AddSubmonoid.LocalizationMap.ofAddEquivOfDom_apply, MonomialOrder.degree_smul_le, AddEquiv.bijective, FreeAddMonoid.freeAddMonoidCongr_of, AddEquiv.mulOp_symm_apply, AddSubmonoid.add_leftNegEquiv, SubAddAction.ofFixingAddSubgroup_insert_map_bijective, AddAut.conj_inv_apply, ZMod.AddAutEquivUnits_apply, AddEquiv.comp_right_injective, IsAddKleinFour.nonempty_addEquiv, AddEquiv.toMultiplicativeLeft_symm_apply_symm_apply, MonoidAlgebra.mapRangeAddEquiv_apply, AddEquiv.coprodAssoc_symm_apply_inr_inr, AddEquiv.mapMatrix_apply, groupCohomology.norm_ofAlgebraAutOnUnits_eq, MonomialOrder.degree_mul_le, AddEquiv.symm_bijective, AddSubmonoid.leftNegEquiv_symm_add, CategoryTheory.InducedCategory.homAddEquiv_symm_apply_hom, AddEquiv.coe_refl, Rep.toAdditive_apply, AddEquiv.eq_comp_symm, CochainComplex.HomComplex.CohomologyClass.equiv_toSmallShiftedHom_mk, SemimoduleCat.homAddEquiv_apply, DirectSum.addEquivProdDirectSum_apply, AddEquiv.comapAddSubgroup_apply, MonomialOrder.le_add_right, AddEquiv.mulOp_apply, AddEquiv.toMultiplicativeRight_symm_apply_apply, AddSubmonoid.LocalizationMap.ofAddEquivOfLocalizations_apply, AddEquiv.coe_trans, AddSubgroup.addSubgroupOfEquivOfLe_symm_apply_coe_coe, MonomialOrder.degree_pow_le, AddEquiv.piAdditive_symm_apply, AddSubsemigroup.strictMono_topEquiv, AddSubmonoid.leftNegEquiv_symm_fromLeftNeg, DirectSum.addEquivProdDirectSum_symm_apply_support', AddSubmonoid.leftNegEquiv_apply, AddSubgroup.comap_toAddSubmonoid, groupHomology.H1AddEquivOfIsTrivial_single, Relation.cutExpand_le_invImage_lex, Finsupp.liftAddHom_apply, MonomialOrder.toSyn_monotone, AddSubsemigroup.map_equiv_eq_comap_symm, SubAddAction.ofFixingAddSubgroup_of_eq_apply, starL_symm_apply, AddEquiv.coprodAssoc_apply_inl_inr, AddEquiv.coprodCongr_apply, WeierstrassCurve.Jacobian.Point.toAffineAddEquiv_apply, MonomialOrder.degLex_single_le_iff, AddSubgroup.topEquiv_symm_apply_coe, CategoryTheory.Abelian.Ext.homAddEquiv_apply, SkewMonoidAlgebra.toFinsuppAddEquiv_symm_apply, AddEquiv.apply_symm_apply, AddLocalization.addEquivOfQuotient_apply, QuotientAddGroup.quotientAddEquivOfEq_mk, uliftMultiplesHom_apply_apply, AddEquiv.toMultiplicative_apply_apply, Finsupp.sumFinsuppAddEquivProdFinsupp_apply, Finset.mapRange_finsuppAntidiag_subset, AddEquiv.equivLike_neg_eq_symm, AddEquiv.strictMono_subsemigroupCongr, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_apply, FreeAddGroup.freeAddGroupCongr_apply, AddEquiv.prodAdditive_apply, AddMonoidHom.toAddEquiv_apply, AlgEquiv.op_symm_apply_symm_apply, AddSubsemigroup.map_equiv_top, AddEquiv.coe_addSubgroupMap_apply, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_pow, Multiset.toFinsupp_singleton, Matrix.conjTransposeAddEquiv_apply, AlternatingMap.domDomCongrEquiv_apply, AddGroupExtension.Equiv.rightHom_comm, AddSubsemigroup.coe_equivMapOfInjective_apply, Multiset.toFinsupp_symm_apply, FreeAbelianGroup.equivFinsupp_apply, CategoryTheory.Abelian.Ext.biprodAddEquiv_apply_fst, AddEquiv.ofBijective_apply, AddEquiv.cast_apply, AddSubmonoid.topEquiv_symm_apply_coe, AddLocalization.addEquivOfQuotient_mk, Representation.ofModule_asModule_act, CategoryTheory.InducedCategory.homAddEquiv_apply, CategoryTheory.Adjunction.compPreadditiveYonedaIso_hom_app_app_apply, AddEquiv.congr_arg, Matrix.piAddEquiv_symm_apply, QuadraticForm.dualProdIsometry_toFun, QuotientAddGroup.quotientKerEquivOfRightInverse_symm_apply, HahnSeries.addOppositeEquiv_orderTop, AddEquiv.coprodAssoc_symm_apply_inl, AddOpposite.coe_opAddEquiv, AddEquiv.punitCoprod_symm_apply, AddEquiv.symmEquiv_symm_apply_apply, starL'_symm_apply, AddSubgroup.centerCongr_symm_apply_coe, AddEquiv.prodAdditive_symm_apply, CochainComplex.HomComplex.Cocycle.rightShiftAddEquiv_symm_apply, FreeAddMonoid.freeAddMonoidCongr_symm_of, AddEquiv.coe_prodComm, AddEquiv.coe_toEquiv_symm, AddEquiv.surjective, AddEquiv.coe_prodAssoc_symm, AddLocalization.addEquivOfQuotient_symm_mk', AddEquiv.addDissociated_preimage, AddAut.coe_one, RestrictScalars.lsmul_apply_apply, AddEquiv.coe_addMonoidHom_trans, groupHomology.H1AddEquivOfIsTrivial_symm_apply, AddEquiv.toMultiplicativeRight_symm_apply_symm_apply, AddAut.mulRight_apply, AddChar.coe_doubleDualEquiv, Finsupp.coe_orderIsoMultiset_symm, SubAddAction.ofStabilizer.conjMap_bijective, AddEquiv.addOrderOf_eq, Finsupp.fst_sumFinsuppAddEquivProdFinsupp, Matrix.transposeAddEquiv_apply, coe_addEquiv_lpBCF_symm, AddEquiv.toMultiplicative_symm_apply_apply, DistribMulAction.toAddEquiv_apply, MulEquiv.toAdditive_symm_apply_apply, addEquivOfAddOrderOfEq_symm_apply_gen, SubAddAction.ofFixingAddSubgroup_insert_map_apply, Subalgebra.algEquivOpMop_apply, AddEquiv.toAddHom_eq_coe, AddEquiv.addSubmonoidMap_symm_apply, AddSubmonoid.topEquiv_apply, Complex.equivRealProdAddHom_apply, AddSubmonoid.equivMapOfInjective_coe_addEquiv, AddEquiv.toAddMonoidHom_injective, MonomialOrder.toSyn_eq_zero_iff, AddAut.conj_apply, AddOpposite.coe_symm_opAddEquiv, QuotientAddGroup.quotientBot_apply, AddSubsemigroup.centerCongr_symm_apply_coe, AddEquiv.symm_trans_apply, AddEquiv.mapAddSubgroup_apply, AlgEquiv.subalgebraMap_apply_coe, coe_ofLexAddEquiv, QuotientAddGroup.quotientKerEquivOfRightInverse_apply, AddEquiv.symm_comp_self, uliftZMultiplesHom_apply_apply, Multiset.toFinsupp_zero, CochainComplex.HomComplex.Cocycle.equivHomShift'_apply, AddEquiv.opOp_symm_apply, Multiset.toFinsupp_toMultiset, MonomialOrder.degree_prod_le, RestrictScalars.addEquiv_symm_map_smul_smul, RingEquiv.op_symm_apply_symm_apply, WithConv.addEquiv_apply, RingEquiv.nonUnitalSubsemiringMap_symm_apply_coe, AddSubgroup.mem_map_equiv, MonomialOrder.div_set, AddMonoidAlgebra.mapDomainRingEquiv_single, CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv_symm_apply, HahnSeries.addOppositeEquiv_symm_orderTop, DFinsupp.comp_liftAddHom, AddEquiv.symm_apply_eq, AddEquiv.map_add, AddEquiv.ext_iff, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_apply, AddMonoidAlgebra.domCongr_support, coe_addEquiv_lpBCF, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_zpow', MonomialOrder.degLex_lt_iff, Finsupp.mapRange.addEquiv_toAddMonoidHom, QuaternionAlgebra.coe_symm_addEquivProd, MulOpposite.opAddEquiv_toEquiv, Nat.factorization_eq_primeFactorsList_multiset, AddEquiv.opOp_apply, AddSubmonoid.LocalizationMap.addEquivOfLocalizations_left_neg_apply, CategoryTheory.InjectiveResolution.extMk_hom, AddAut.inv_apply, AddEquiv.ofLeftInverse'_symm_apply, SubAddAction.fixingAddSubgroupEquivFixingAddSubgroup_coe_apply, groupHomology.H1AddEquivOfIsTrivial_apply, AddSubgroup.centerToAddOpposite_symm_apply_coe, AddSubmonoid.centerCongr_apply_coe, AddEquiv.injective, AddOpposite.opAddEquiv_symm_apply, Rep.unit_iso_comm, AddEquiv.toMultiplicative_symm_apply_symm_apply, CategoryTheory.Adjunction.homAddEquiv_symm_apply, AddEquiv.apply_eq_iff_eq, AddEquiv.congr_fun, Multiset.toFinsupp_eq_iff, AddEquiv.val_piAddUnits_symm_apply, AddEquiv.cast_symm_apply, AddMonoid.IsTorsion.torsionAddEquiv_apply, AddEquiv.additiveMultiplicative_symm_apply, AddLocalization.addEquivOfQuotient_symm_mk, DistribMulAction.toAddEquiv_symm_apply, Unitization.isUniformEmbedding_addEquiv, AddEquiv.toEquiv_injective, DirectSum.equivCongrLeft_apply, AddEquiv.coe_symm_toNatLinearEquiv, Finsupp.liftAddHom_singleAddHom, AddEquiv.finsuppUnique_symm_apply_support_val, HahnSeries.addOppositeEquiv_symm_leadingCoeff, CategoryTheory.Abelian.Ext.addEquiv₀_symm_apply, HahnSeries.addOppositeEquiv_leadingCoeff, Finsupp.domLCongr_apply, AddSubgroup.topEquiv_apply, AddEquiv.instAddEquivClass, AddAction.stabilizerEquivStabilizer_apply, AddEquiv.toEquiv_eq_coe, DFinsupp.liftAddHom_singleAddHom, Representation.ofModule_asAlgebraHom_apply_apply, QuotientAddGroup.quotientBot_symm_apply, MulEquiv.toAdditive_symm_apply_symm_apply, Finsupp.lift_symm_apply, AddSubmonoid.LocalizationMap.ofAddEquivOfDom_comp_symm, coe_addEquiv_lpPiLp, AddEquiv.toAdditive_toMultiplicative_apply, AddEquiv.coe_toIntLinearEquiv, AddEquiv.addSubgroupCongr_symm_apply, AddLocalization.addEquivOfQuotient_addMonoidOf, AddAut.symm_inv, MulEquiv.toAdditive_apply_symm_apply, AddAut.mulLeft_apply_apply, AddEquiv.coe_toEquiv, AddSubgroup.equivMapOfInjective_coe_addEquiv, CochainComplex.HomComplex.Cocycle.equivHomShift_comp, AddEquiv.ext_int_iff, AddEquiv.coe_addMonoidHom_symm_comp_coe_addMonoidHom, Finsupp.liftAddHom_apply_single, AddLocalization.addEquivOfQuotient_symm_addMonoidOf, SubAddAction.ofStabilizer.neg_conjMap_comp_apply, ContinuousAddEquiv.coe_mk, AddGroupExtension.Equiv.coe_toAddEquiv, CochainComplex.HomComplex.Cocycle.equivHom_apply, AlgEquiv.opComm_symm_apply_symm_apply, AddEquiv.symmEquiv_apply_apply, DirectSum.decomposeAddEquiv_symm_apply, MonoidAlgebra.mapRangeAddEquiv_single, MulAutMultiplicative_apply_symm_apply, AddChar.doubleDualEquiv_symm_doubleDualEmb_apply, WithLp.coe_addEquiv, AddEquiv.subsemigroupMap_symm_apply_coe, MonomialOrder.lex_lt_iff, AddEquiv.refl_apply, DirectSum.decomposeAddEquiv_apply, AddSubmonoid.LocalizationMap.ofAddEquivOfDom_comp, AddMonoidAlgebra.mapRangeAddEquiv_single, finsuppAddEquivDFinsupp_apply, ContinuousMap.addEquivBoundedOfCompact_symm_apply, AddMonoidAlgebra.domCongr_apply, AddEquiv.coe_toNatLinearEquiv, AddSubgroup.map_symm_eq_iff_map_eq, finsuppAddEquivDFinsupp_symm_apply, AddAut.one_apply, AddEquiv.trans_apply, AddSubsemigroup.topEquiv_toAddHom, AddGroupExtension.Equiv.inl_comm, Finsupp.liftAddHom_symm_apply_apply, AddEquiv.toMultiplicativeLeft_symm_apply_apply, Subsemiring.ringEquivOpMop_apply, CategoryTheory.Abelian.Ext.addEquivBiprod_symm_apply, AddEquiv.coprodAssoc_apply_inl_inl, Unitization.antilipschitzWith_addEquiv, AddEquiv.map_finsum, AddEquiv.neg'_symm_apply, AddEquiv.finite_left, AddCon.quotientKerEquivOfRightInverse_apply, LinearEquiv.arrowCongrAddEquiv_apply, AddCon.comapQuotientEquivOfSurj_symm_mk', Finsupp.sumFinsuppAddEquivProdFinsupp_symm_inr, HahnSeries.addOppositeEquiv_symm_apply_coeff, AddEquiv.val_neg_piAddUnits_symm_apply, Finsupp.curryAddEquiv_symm_apply, Finsupp.liftAddHom_symm_apply, CochainComplex.HomComplex.Cochain.leftShiftAddEquiv_symm_apply, AddEquiv.eq_iff_eq_on_generator, IsPrimitiveRoot.zmodEquivZPowers_apply_coe_nat, AddSubmonoid.map_equiv_eq_comap_symm, AddAut.mulLeft_apply_symm_apply, AddEquiv.eq_symm_apply, MonomialOrder.div, WeierstrassCurve.Jacobian.Point.toAffineAddEquiv_symm_apply, toEquiv_toLexAddEquiv, DFinsupp.liftAddHom_comp_single, MonomialOrder.lex_le_iff, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_precomp, addMonoidAlgebraAddEquivDirectSum_symm_apply, AddEquiv.coprodCongr_symm_apply, AddEquiv.finsuppUnique_symm_apply_apply, AddEquiv.prodUnique_symm_apply, AddEquiv.coe_mk, zmultiplesAddHom_apply, MonomialOrder.degree_sPolynomial_le, AddEquiv.coprodComm_symm_apply, FreeAbelianGroup.liftAddEquiv_apply_apply, CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv_apply, Equiv.addEquiv_symm_apply, CategoryTheory.Adjunction.homAddEquiv_apply, SkewMonoidAlgebra.domCongr_apply, AddCon.comapQuotientEquivOfSurj_mk, WithLp.addEquiv_symm_apply, CochainComplex.HomComplex.Cocycle.rightShiftAddEquiv_apply, MonomialOrder.degree_sub_leadingTerm_lt_degree, AddChar.doubleDualEmb_doubleDualEquiv_symm_apply, toAddUnits_symm_apply, MonoidAlgebra.mapDomainAddEquiv_apply, CochainComplex.HomComplex.Cocycle.equivHomShift_comp_shift, HahnSeries.addOppositeEquiv_apply, LinearEquiv.arrowCongrAddEquiv_symm_apply, addMonoidAlgebraAddEquivDirectSum_apply, MonomialOrder.degree_monomial_le, Unitization.uniformity_eq_aux, SubAddAction.ofStabilizer.conjMap_comp_apply, MonomialOrder.degLex_single_lt_iff, AddUnits.coe_opEquiv_symm, ModuleCat.homAddEquiv_apply, CategoryTheory.Abelian.Ext.addEquivBiprod_apply_snd, Unitization.lipschitzWith_addEquiv, Subsemiring.mopRingEquivOp_symm_apply, MonomialOrder.degree_sub_LTerm_lt, MonomialOrder.sPolynomial_lt_of_degree_ne_zero_of_degree_eq, WeierstrassCurve.Projective.Point.toAffineAddEquiv_symm_apply, AlgEquiv.subalgebraMap_symm_apply_coe, AddEquiv.coe_toAddHom, ModuleCat.semilinearMapAddEquiv_symm_apply_apply, AddEquiv.coprodAssoc_symm_apply_inr_inl, AddEquiv.map_sub, Nat.Partition.coeff_genFun, RestrictScalars.addEquiv_symm_map_algebraMap_smul, AddCircle.equivAddCircle_symm_apply_mk, AddAut.smul_def, AddSubsemigroup.centerToAddOpposite_apply_coe, CategoryTheory.Abelian.Ext.biprodAddEquiv_symm_apply, AddEquiv.op_symm_apply_apply, RingEquiv.nonUnitalSubsemiringMap_apply_coe, AddAut.neg_conj_apply, CochainComplex.HomComplex.Cochain.toSingleEquiv_toSingleMk, starAddEquiv_apply, AddEquiv.map_neg, DFinsupp.liftAddHom_symm_apply, AddEquiv.addMonoidHomCongrRight_apply, toAddUnits_val_apply, AddChar.zmodAddEquiv_apply, AddCon.congr_mk, Subring.ringEquivOpMop_apply, AddEquiv.piCongrRight_apply, groupHomology.H1AddEquivOfIsTrivial_symm_tmul, AddEquiv.coe_toAddMonoidHom, AddCon.quotientKerEquivOfRightInverse_symm_apply, Matrix.coe_ofAddEquiv, CochainComplex.HomComplex.CohomologyClass.toHom_mk, AddAction.stabilizerEquivStabilizer_compTriple, AddEquiv.uniqueProd_apply, IsPrimitiveRoot.zmodEquivZPowers_apply_coe_int, CochainComplex.HomComplex.Cocycle.leftShiftAddEquiv_apply, Multiset.toFinsupp_support, MulOpposite.opAddEquiv_symm_apply, ModuleCat.semilinearMapAddEquiv_apply, QuaternionAlgebra.coe_addEquivTuple, AddEquiv.apply_eq_iff_symm_apply, AddEquiv.finite_right, CategoryTheory.Abelian.Ext.addEquivBiprod_apply_fst, AddSubmonoid.mem_map_equiv, coe_toLexAddEquiv, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, AddEquiv.ofBijective_apply_symm_apply, AddAutAdditive_symm_apply_apply, AddEquiv.val_piAddUnits_apply, Multiset.toFinsupp_strictMono, AddEquiv.toFun_eq_coe, MonomialOrder.degree_sPolynomial_lt_sup_degree, AddEquiv.ofLeftInverse_symm_apply, CochainComplex.HomComplex.Cocycle.equivHomShift_apply, AddCommGrpCat.homAddEquiv_apply, AddSubmonoid.topEquiv_toAddMonoidHom, MonomialOrder.degree_sub_leadingTerm_lt_iff, AddEquivClass.toAddEquiv_injective, MonomialOrder.degree_sub_leadingTerm_le, Matrix.piAddEquiv_apply, AlternatingMap.domDomCongrEquiv_symm_apply, CategoryTheory.Abelian.Ext.biprodAddEquiv_apply_snd, WithLp.coe_symm_addEquiv, Matrix.compAddEquiv_symm_apply, AddSubmonoid.leftNegEquiv_symm_eq_neg, CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_symm_apply, Matrix.compAddEquiv_apply, LinearEquiv.coe_addEquiv_apply, AddEquiv.toMultiplicativeLeft_apply_apply, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_zpow, AddEquiv.op_apply_symm_apply, RestrictScalars.smul_def, toEquiv_ofLexAddEquiv, AddMonoidHom.ofInjective_apply, Subring.addEquivOp_symm_apply_coe, QuaternionAlgebra.coe_symm_addEquivTuple, AddEquiv.comapAddSubgroup_symm_apply, Rep.indResHomEquiv_symm_apply_hom, AddEquiv.punitCoprod_apply, Finsupp.toMultiset_eq_iff, AddAut.inv_apply_self, MonomialOrder.degree_sub_LTerm_le, MonomialOrder.lex_le_iff_of_unique, CochainComplex.HomComplex.CohomologyClass.homAddEquiv_apply, RestrictScalars.addEquiv_map_smul, CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_apply, AddSubmonoid.centerToAddOpposite_apply_coe, MultilinearMap.domDomCongrEquiv_apply, MonomialOrder.degree_sPolynomial, SemimoduleCat.homAddEquiv_symm_apply_hom, AddSubmonoid.LocalizationMap.addEquivOfLocalizations_apply, AddEquiv.coe_symm_toIntLinearEquiv, MonomialOrder.degree_X_le_single, CategoryTheory.Iso.addCommGroupIsoToAddEquiv_apply, AddEquiv.op_apply_apply, AddEquiv.eq_symm_comp, SubAddAction.ofStabilizer.conjMap_apply, uliftZMultiplesHom_symm_apply
AddEquivClass 📖	CompData	6 math math: ContinuousAddEquiv.instAddEquivClass, RingEquivClass.toAddEquivClass, OrderAddMonoidIso.instAddEquivClass, AddEquiv.instAddEquivClass, SemilinearEquivClass.toAddEquivClass, AddGroupExtension.Equiv.instAddEquivClass
MulEquiv 📖	CompData	728 math math: MonoidAlgebra.mapDomainRingEquiv_single, Submonoid.mem_map_equiv, ConjAct.smul_def, SubMulAction.ofStabilizer.conjMap_comp_apply, FreeMonoid.freeMonoidCongr_of, SubMulAction.ofFixingSubgroup_insert_map_apply, ContinuousLinearEquiv.unitsEquiv_apply, ConjAct.toConjAct_inv, MulAut.symm_inv, ValuationSubring.coe_mem_principalUnitGroup_iff, Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_apply, galRestrict_symm_algebraMap_apply, Subgroup.equivSMul_apply_coe, MulEquiv.map_eq_one_iff, MulAut.one_apply, ConjAct.toConjAct_mul, FreeGroupBasis.repr_apply_coe, Ideal.exists_comap_galRestrict_eq, MulEquiv.coe_trans, Subgroup.centerCongr_symm_apply_coe, zpowersMulHom_symm_apply, MulEquiv.monoidHomCongrLeft_apply, rootsOfUnityEquivOfPrimitiveRoots_apply_coe_inv_val, CategoryTheory.Iso.conjAut_apply, AddEquiv.toMultiplicative_apply_symm_apply, MulEquiv.coe_monoidHom_symm_comp_coe_monoidHom, autAdjoinRootXPowSubCEquiv_root, CoxeterMatrix.reindex_relationsSet, Subgroup.equivMapOfInjective_coe_mulEquiv, MonoidHom.restrictHomKerEquiv_apply_coe, NumberField.IsCMField.unitsComplexConj_torsion, ConjAct.stabilizer_eq_centralizer, MulEquiv.inv'_apply, Subgroup.comap_equiv_eq_map_symm, WithZero.withZeroUnitsEquiv_symm_apply_coe, mulEquivOfOrderOfEq_symm_apply_gen, MulEquiv.prodProdProdComm_apply, AddAutAdditive_apply_symm_apply, MulAut.inv_apply, Submonoid.mul_leftInvEquiv, CategoryTheory.InducedCategory.endEquiv_symm_apply_hom, StarMulEquiv.coe_mk, CategoryTheory.InducedCategory.endEquiv_apply, MulAut.conjNormal_symm_apply, Ideal.coe_smul_primesOver_mk_eq_map_galRestrict, SubMulAction.ofStabilizer.conjMap_comp_inv_apply, WithZero.coe_unitsWithZeroEquiv_eq_units_val, val_inv_unitarySubgroupUnitsEquiv_symm_apply_coe, Submonoid.leftInvEquiv_symm_mul, Subsemigroup.centerToMulOpposite_apply_coe, CategoryTheory.Iso.commGroupIsoToMulEquiv_symm_apply, OrderMonoidIso.withZero_symm_apply_symm_apply, IsCyclic.val_mulAutMulEquiv_apply, CongruenceSubgroup.exists_Gamma_le_conj', Unitary.conjStarAlgEquiv_unitaryLinearIsometryEquiv, unitsNonZeroDivisorsEquiv_apply, MulEquiv.toAdditive_apply_apply, MulEquiv.symm_comp_self, AddEquiv.toMultiplicativeRight_apply_apply, Submonoid.fromLeftInv_leftInvEquiv_symm, MulAction.stabilizerEquivStabilizer_symm_apply, CongruenceSubgroup.conjGL_coe, MulEquiv.map_one, Subgroup.isCoatom_map, associatesEquivOfUniqueUnits_symm_apply, SemidirectProduct.inl_aut, MulEquiv.piMultiplicative_apply, CommGroup.monoidHom_mulEquiv_of_hasEnoughRootsOfUnity, Subsemigroup.centerCongr_symm_apply_coe, OrderMonoidIso.val_unitsCongr_symm_apply, Submonoid.LocalizationMap.mulEquivOfLocalizations_apply, MulEquiv.eq_symm_apply, Subgroup.comap_toSubmonoid, InfiniteGalois.normalAutEquivQuotient_apply, CategoryTheory.Functor.FullyFaithful.homMulEquiv_apply, IsGaloisGroup.mulEquivAlgEquiv_apply_symm_apply, MonoidAlgebra.domCongr_toAlgHom, Set.unitEquivUnitsInteger_symm_apply_coe, Equiv.Perm.val_equivUnitsEnd_apply, CategoryTheory.PreGaloisCategory.toAutMulEquiv_isHomeomorph, Localization.mulEquivOfQuotient_symm_monoidOf, CategoryTheory.Iso.refl_conj, val_unitarySubgroupUnitsEquiv_symm_apply_coe, MulEquiv.comapSubgroup_symm_apply, toEquiv_toLexMulEquiv, MulDistribMulAction.toMulEquiv_apply, autEquivZmod_symm_apply_natCast, Matrix.GeneralLinearGroup.coe_toLin, MulEquiv.toMonoidHom_eq_coe, map_dvd_iff_dvd_symm, MulEquiv.toSingleObjEquiv_inverse_map, Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_symm_apply_coe_coe, NonUnitalSubsemiring.centerCongr_symm_apply_coe, CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_symm_apply_hom, autAdjoinRootXPowSubCEquiv_symm_smul, MonoidHom.ofLeftInverse_symm_apply, AddAutAdditive_apply_apply, IsCyclic.monoidHom_mulEquiv_rootsOfUnity, AddOpposite.opMulEquiv_symm_apply, SubMulAction.ofStabilizer.inv_conjMap_comp_apply, Unitary.coe_linearIsometryEquiv_apply, MulEquiv.coe_refl, ConjAct.forall, HNNExtension.equiv_eq_conj, LinearMap.GeneralLinearGroup.generalLinearEquiv_to_linearMap, uliftZPowersHom_symm_apply, MulEquiv.map_div, AddAutAdditive_symm_apply_symm_apply, CategoryTheory.Iso.conj_pow, Subsemiring.centerCongr_symm_apply_coe, Unitary.linearIsometryEquiv_coe_apply, MulEquiv.finite_left, CategoryTheory.Iso.conjAut_mul, MulAut.smul_def, MulEquiv.coe_submonoidMap_apply, MulEquiv.prodMultiplicative_symm_apply, MulEquiv.val_piUnits_symm_apply, val_unitsCentralizerEquiv_apply_coe, SpecialLinearGroup.centerCongr_toLin_equiv_trans_centerEquivRootsOfUnity_eq, Equiv.altCongrHom_apply_coe, RingEquiv.coe_toMulEquiv, Submonoid.equivMapOfInjective_coe_mulEquiv, IsCusp.of_isFiniteRelIndex_conj, ConjAct.toConjAct_zero, MulAutMultiplicative_symm_apply_apply, MulAut.mul_apply, MulEquiv.opOp_symm_apply, MulEquiv.comp_symm_eq, MulEquiv.mapSubgroup_apply, MulEquiv.op_apply_symm_apply, MulEquiv.map_finprod, RootPairing.Equiv.toEndUnit_inv, MulEquiv.comp_right_injective, MulEquiv.apply_eq_iff_eq, ZMod.AddAutEquivUnits_symm_apply, starMulAut_apply, HNNExtension.inv_t_mul_of, QuotientGroup.liftEquiv_coe, MulEquiv.eq_symm_comp, MulAutMultiplicative_apply_apply, Submonoid.LocalizationMap.ofMulEquivOfDom_comp_symm, MulChar.mulEquiv_units, MulAut.inv_apply_self, SlashInvariantForm.coe_translate, Submonoid.topEquiv_symm_apply_coe, Subgroup.coe_equivMapOfInjective_apply, AddEquiv.toMultiplicativeLeft_apply_symm_apply, Submonoid.map_coe_toMulEquiv, QuotientGroup.quotientKerEquivOfRightInverse_apply, Equiv.permCongrHom_coe, coe_galRestrict_apply, ModularGroup.lcRow0Extend_symm_apply, Subgroup.conjAct_pointwise_smul_iff, MulEquiv.coprodPUnit_symm_apply, MulAction.stabilizerEquivStabilizer_compTriple, MulEquiv.invFun_eq_symm, CoxeterSystem.getElem_succ_leftInvSeq_alternatingWord, OrderMonoidIso.coe_mulEquiv, CommGroup.equiv_prod_multiplicative_zmod_of_finite, CategoryTheory.Aut.toEnd_apply, AffineEquiv.linear_equivUnitsAffineMap_symm_apply, uliftPowersHom_symm_apply, MulEquiv.coprodAssoc_symm_apply_inr_inr, Subgroup.centerCongr_apply_coe, Monoid.IsTorsion.torsionMulEquiv_apply, MulEquiv.prodMultiplicative_apply, Subgroup.mem_map_equiv, unitarySubgroupUnitsEquiv_apply_coe, Submonoid.centerToMulOpposite_apply_coe, AddEquiv.toMultiplicativeRight_apply_symm_apply, zpowersMulHom_apply, Subsemigroup.topEquiv_symm_apply_coe, val_toUnits_apply, MulAut.coe_inv, MulEquiv.instMulEquivClass, MonoidAlgebra.domCongr_single, unitary.linearIsometryEquiv_coe_symm_apply, MulEquiv.withZero_apply_symm_apply, QuotientGroup.liftEquiv_mk, MulAut.coe_one, MulEquiv.subgroupCongr_apply, SemidirectProduct.congr'_apply_right, OrderMonoidIso.val_inv_unitsCongr_symm_apply, lipschitzGroup.conjAct_smul_ι_mem_range_ι, FreeGroupBasis.lift_apply_apply, Subgroup.centerToMulOpposite_apply_coe, MulEquiv.ofLeftInverse_symm_apply, CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_apply_inv, spinGroup.units_involute_act_eq_conjAct, Semigrp.mulEquiv_coe_eq, CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_apply_hom, IsGaloisGroup.mulEquivCongr_apply_smul, DirichletCharacter.mulEquiv_units, Con.comapQuotientEquivOfSurj_symm_mk', Subgroup.Commensurable.commensurator_mem_iff, Subgroup.map_symm_eq_iff_map_eq, algebraMap_galRestrict_apply, val_inv_unitsNonZeroDivisorsEquiv_symm_apply_coe, spinGroup.conjAct_smul_ι_mem_range_ι, comap_upperCentralSeries, Unitary.coe_symm_linearIsometryEquiv_apply, CategoryTheory.Iso.trans_conjAut, Submonoid.leftInvEquiv_apply, MulEquiv.toMonoidWithZeroHom_apply, MulAutMultiplicative_symm_apply_symm_apply, MulEquiv.toSingleObjEquiv_unitIso_hom, MulEquiv.strictMono_subsemigroupCongr, Equiv.mulEquiv_apply, OrderMonoidIso.coe_mk, Submonoid.val_inv_unitsTypeEquivIsUnitSubmonoid_symm_apply, MulEquiv.coprodPUnit_apply, Nonneg.val_unitsEquivPos_symm_apply_coe, spinGroup.conjAct_smul_range_ι, SpecialLinearGroup.congr_linearEquiv_coe_apply, ConjAct.ofConjAct_zero, MonoidHom.restrictHomKerEquiv_symm_coe_apply, monoidEndToAdditive_apply_apply, MulEquiv.eq_comp_symm, CategoryTheory.Functor.map_conj, MulEquiv.withZero_apply_apply, Con.comapQuotientEquivOfSurj_mk, CategoryTheory.Functor.map_conjAut, GrpWithZero.Iso.mk_hom, MulEquiv.coe_prodAssoc, InfiniteGalois.mulEquivToLimit_symm_continuous, CongruenceSubgroup.IsArithmetic.conj, IsCyclic.val_inv_mulAutMulEquiv_apply, Subsemigroup.topEquiv_toMulHom, MulEquiv.arrowCongr_apply, WithZero.withZeroUnitsEquiv_symm_strictMono, ModularGroup.lcRow0Extend_apply, MulEquiv.coprodAssoc_apply_inl_inl, Monoid.PushoutI.NormalWord.cons_head, Submonoid.leftInvEquiv_mul, MulEquiv.restrictRootsOfUnity_coe_apply, MulEquiv.prodUnique_symm_apply, Localization.mulEquivOfQuotient_mk, OrderMonoidIso.withZero_apply_symm_apply, MulAction.stabilizerEquivStabilizer_apply, MulEquiv.coe_prodComm_symm, InfiniteGalois.isOpen_mulEquivToLimit_image_fixingSubgroup, associatesNonZeroDivisorsEquiv_mk_mk, MulEquiv.map_inv, WithZero.unitsWithZeroEquiv_symm_apply, ValuationSubring.coe_unitGroupMulEquiv_apply, Subgroup.subgroupOfEquivOfLe_symm_apply_coe_coe, autEquivZmod_symm_apply_intCast, ConjAct.units_smul_def, AffineEquiv.val_equivUnitsAffineMap_apply, MonoidHom.toMulEquiv_symm_apply, CategoryTheory.PreGaloisCategory.toAutMulEquiv_apply, MulOpposite.coe_symm_opMulEquiv, associatesNonZeroDivisorsEquiv_symm_mk_mk, IsGalois.normalAutEquivQuotient_apply, UniqueFactorizationMonoid.normalizedFactorsEquiv_symm_apply, MulEquiv.val_inv_piUnits_apply, MulEquiv.apply_eq_iff_symm_apply, CategoryTheory.SingleObj.toEnd_def, Matrix.GeneralLinearGroup.toLin'_apply, IsFreeGroup.toFreeGroup_symm_apply, CongruenceSubgroup.isArithmetic_conj_SL2Z, QuotientGroup.quotientKerEquivOfRightInverse_symm_apply, Submonoid.unitsTypeEquivIsUnitSubmonoid_apply_coe, WithZero.toMulBot_lt, HNNExtension.NormalWord.unitsSMul_one_group_smul, coe_ofLexMulEquiv, MulEquiv.self_comp_symm, MulEquiv.coprodAssoc_apply_inl_inr, SemidirectProduct.congr'_apply_left, CoxeterSystem.rightInvSeq_concat, IsGaloisGroup.mulEquivAlgEquiv_apply_apply, MulEquiv.symm_apply_eq, MulEquiv.toSingleObjEquiv_counitIso_hom, MulAut.coe_mul, IsCyclic.monoidHom_equiv_self, MulEquiv.withOneCongr_apply, SpecialLinearGroup.centerEquivRootsOfUnity_symm_apply, MulEquiv.coe_toMonoidHom, pinGroup.conjAct_smul_ι_mem_range_ι, Unitization.val_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, SemidirectProduct.congr'_symm_apply_right, MulEquiv.AddMonoid.End_apply, MulEquiv.ofLeftInverse'_apply, mkFactorOrderIsoOfFactorDvdEquiv_apply_coe, Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, val_unitsNonZeroDivisorsEquiv_symm_apply_coe, NonUnitalSubring.centerCongr_symm_apply_coe, SemidirectProduct.mul_def, MulEquiv.prodUnique_apply, ZMod.AddAutEquivUnits_apply, Subgroup.val_centerUnitsEquivUnitsCenter_symm_apply_coe, MulEquiv.prodProdProdComm_toEquiv, MulEquiv.coprodCongr_apply, Monoid.IsTorsion.torsionMulEquiv_symm_apply_coe, MulHom.toMulEquiv_symm_apply, AddEquiv.toMultiplicativeLeft_symm_apply_symm_apply, Submonoid.centerToMulOpposite_symm_apply_coe, mulAutArrow_apply_apply, CategoryTheory.Functor.FullyFaithful.mulEquivEnd_symm_apply, MulEquiv.ofLeftInverse_apply, Localization.mulEquivOfQuotient_mk', MulEquiv.toMultiplicative_toAdditive_symm_apply, Subsemigroup.strictMono_topEquiv, CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_symm_app, MonoidAlgebra.toRingHom_mapDomainRingEquiv, HNNExtension.of_mul_t, MulEquiv.congr_fun, Subgroup.topEquiv_symm_apply_coe, Unitary.linearIsometryEquiv_coe_symm_apply, Subgroup.normalizerMonoidHom_apply_apply_coe, MulEquiv.congr_arg, CuspForm.coe_translate, HNNExtension.of_mul_inv_t, AddEquiv.toMultiplicativeRight_symm_apply_apply, OrderMonoidIso.withZero_apply_apply, IsKleinFour.nonempty_mulEquiv, MulEquiv.surjective, MulEquiv.toSingleObjEquiv_unitIso_inv, Set.val_unitEquivUnitsInteger_apply_coe, WithZero.toMulBot_coe_ofAdd, Submonoid.LocalizationMap.ofMulEquivOfDom_comp, SubMulAction.ofFixingSubgroup_of_eq_apply, MulOpposite.opMulEquiv_apply, Ideal.Quotient.stabilizerQuotientInertiaEquiv_mk, MulEquiv.cast_symm_apply, IsCyclotomicExtension.Rat.galEquivZMod_apply_of_pow_eq, Con.quotientKerEquivOfRightInverse_symm_apply, Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_apply, MulEquiv.trans_apply, mulAutArrow_apply_symm_apply, Units.coe_unop_opEquiv, MulEquiv.mapSubgroup_symm_apply, MulEquiv.ext_iff, SemidirectProduct.inl_aut_inv, Subgroup.mem_ofUnits_iff_toUnits_mem, LinearMap.GeneralLinearGroup.congrLinearEquiv_apply, MulEquiv.inv'_symm_apply, starMulEquiv_apply, Units.toAut_hom, MulEquiv.equivLike_inv_eq_symm, CategoryTheory.Groupoid.vertexGroupIsomOfMap_apply, MulAut.conj_apply, MulEquiv.ofBijective_apply_symm_apply, MulEquiv.op_apply_apply, CategoryTheory.Hom.mulEquivCongrRight_symm_apply, MulEquiv.toFun_eq_coe, MulEquiv.uniqueProd_symm_apply, MulEquiv.multiplicativeAdditive_apply, Submonoid.centerCongr_symm_apply_coe, MagmaCat.mulEquiv_coe_eq, AffineEquiv.equivUnitsAffineMap_symm_apply_apply, AddEquiv.toMultiplicative_apply_apply, Unitary.toAlgEquiv_conjStarAlgAut, MulEquiv.coe_mk, groupCohomology.exists_mul_galRestrict_of_norm_eq_one, GroupExtension.Equiv.rightHom_comm, Nonneg.unitsEquivPos_apply_coe, surjective_rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar, MulEquiv.toSingleObjEquiv_counitIso_inv, galRestrictHom_symm_algebraMap_apply, freeGroupEquivCoprodI_symm_apply, Con.comapQuotientEquivOfSurj_symm_mk, GroupExtension.Equiv.inl_comm, Matrix.SpecialLinearGroup.toLin_equiv.symm_toLinearMap_eq, ConjAct.toConjAct_smul, MulHom.toMulEquiv_apply, Subsemigroup.centerToMulOpposite_symm_apply_coe, pinGroup.conjAct_smul_range_ι, MulEquiv.toEquiv_eq_coe, IsCyclotomicExtension.Rat.galEquivZMod_restrictNormal_apply, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply, MulDistribMulAction.toMulEquiv_symm_apply, NumberField.RingOfIntegers.withValEquiv_apply, Localization.mulEquivOfQuotient_symm_mk, AddOpposite.opMulEquiv_toEquiv, val_unitsCentralizerEquiv_symm_apply_coe, isNilpotent_of_finite_tfae, CoxeterMatrix.reindexGroupEquiv_apply_simple, Submodule.unitsQuotEquivRelPic_symm_apply, MulEquiv.coprodAssoc_apply_inr, HNNExtension.t_mul_of, Subgroup.val_centerUnitsEquivUnitsCenter_apply_coe, CommGroup.equiv_free_prod_prod_multiplicative_zmod, MulEquiv.symmEquiv_apply_apply, WithZero.toMonoidWithZeroHom_withZeroUnitsEquiv, MulAut.conj_inv_apply, AlgEquiv.algHomUnitsEquiv_apply_symm_apply, powersMulHom_apply, AddConstEquiv.coe_val_inv_equivUnits_apply, MulEquiv.funUnique_symm_apply, MulEquiv.uniqueProd_apply, MulEquiv.comapSubgroup_apply, WithZero.toMulBot_zero, AlgEquiv.val_algHomUnitsEquiv_symm_apply, CategoryTheory.Functor.FullyFaithful.homMulEquiv_symm_apply, Submonoid.map_equiv_eq_comap_symm, MulEquiv.eq_iff_eq_on_generator, CategoryTheory.yonedaGrpObjIsoOfRepresentableBy_hom, MulEquiv.submonoidMap_symm_apply, Unitary.toRingEquiv_conjStarAlgAut, CategoryTheory.yonedaGrpObjIsoOfRepresentableBy_inv, FGModuleCat.Iso.conj_eq_conj, Set.conj_mem_fixingSubgroup, Submonoid.LocalizationMap.mulEquivOfLocalizations_symm_apply, monoidEndToAdditive_symm_apply_apply, SemidirectProduct.mulEquivProd_symm_apply_left, AddEquiv.toMultiplicativeRight_symm_apply_symm_apply, MonoidAlgebra.domCongr_comp_lsingle, MulEquiv.symm_trans_apply, ContinuousMulEquiv.coe_mk, MulEquiv.punitCoprod_symm_apply, MulEquiv.coprodComm_symm_apply, Subgroup.subgroupOfContinuousMulEquivOfLe_apply, SpecialLinearGroup.centerEquivRootsOfUnity_apply, AffineEquiv.equivUnitsAffineMap_symm_apply_symm_apply, NumberField.IsCMField.unitsMulComplexConjInv_apply, AddEquiv.toMultiplicative_symm_apply_apply, MulEquiv.toAdditive_symm_apply_apply, uliftPowersHom_apply_apply, MulEquiv.multiplicativeAdditive_symm_apply, IsFreeGroup.toFreeGroup_apply, MulEquiv.piUnique_apply, AddConstEquiv.equivUnits_symm_apply_apply, AlgEquiv.opComm_apply_symm_apply, MulEquiv.coe_prodAssoc_symm, Subsemigroup.mem_map_equiv, Con.quotientKerEquivOfRightInverse_apply, CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_symm_apply_inv, ClassGroup.equivPic_symm_apply, CategoryTheory.Groupoid.vertexGroupIsomOfMap_symm_apply, SubMulAction.ofStabilizer.conjMap_comp, Subgroup.index_map_equiv, ConjAct.ofConjAct_toConjAct, RingEquiv.piCongrLeft_apply, AffineEquiv.equivUnitsAffineMap_symm_apply_toFun, SemimoduleCat.Iso.conj_eq_conj, associatesEquivOfUniqueUnits_apply, MulAction.zpowersQuotientStabilizerEquiv_symm_apply, toEquiv_ofLexMulEquiv, MulEquiv.toEquiv_injective, Abelianization.equivOfComm_apply, Submonoid.LocalizationMap.of_mulEquivOfMulEquiv_apply, NumberField.IsCMField.unitsComplexConj_eq_self_iff, HNNExtension.toSubgroupEquiv_neg_apply, SemidirectProduct.congr'_symm_apply_left, CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_π, MulEquiv.symmEquiv_symm_apply_apply, Subsemigroup.map_equiv_eq_comap_symm, MulEquiv.toMultiplicative_toAdditive_apply, GroupExtension.inl_conjAct_comm, Subring.centerCongr_symm_apply_coe, Equiv.Perm.OnCycleFactors.Subgroup.Centralizer.toConjAct_smul_mem_cycleFactorsFinset, ValuationSubring.principalUnitGroupEquiv_apply, AlgEquiv.autCongr_apply, galRestrict_apply, MulAut.conj_symm_apply, MulEquiv.orderOf_eq, MulEquiv.coe_monoidHom_trans, MulEquiv.cast_apply, CategoryTheory.Iso.symm_self_conj, MulEquiv.toMonoidHom_injective, MulEquiv.mulDissociated_preimage, MonoidHom.ofLeftInverse_apply, Matrix.SpecialLinearGroup.eq_scalar_center_equiv_rootsOfUnity, mkFactorOrderIsoOfFactorDvdEquiv_symm_apply_coe, Ideal.coe_smul_primesOver_eq_map_galRestrict, Submonoid.LocalizationMap.ofMulEquivOfLocalizations_apply, Submonoid.LocalizationMap.mulEquivOfLocalizations_left_inv_apply, DomMulAct.stabilizerMulEquiv_apply, MonoidHom.ker_comp_mulEquiv, AddEquiv.toMultiplicative_symm_apply_symm_apply, WithZero.toMulBot_coe, MulEquiv.coprodComm_apply, Subsemigroup.topEquiv_apply, Localization.mulEquivOfQuotient_monoidOf, FreeGroupBasis.lift_symm_apply, MulEquiv.symmEquiv_symm_apply_symm_apply, MulEquiv.toEquiv_symm, Submonoid.powLogEquiv_apply, MulEquivClass.coe_symm_apply_apply, MulEquiv.piUnique_symm_apply, GroupExtension.Equiv.coe_toMulEquiv, Subgroup.conjAct_pointwise_smul_eq_self, Con.congr_mk, Localization.mulEquivOfQuotient_apply, ValuationSubring.coe_unitGroupMulEquiv_symm_apply, Submonoid.LocalizationMap.ofMulEquivOfDom_apply, AlgEquiv.val_inv_algHomUnitsEquiv_symm_apply, LinearOrderedCommGroupWithZero.fst_apply, MulEquivClass.apply_coe_symm_apply, MulEquiv.opOp_apply, MulAut.congr_apply, Submonoid.leftInvEquiv_symm_eq_inv, MulEquivClass.toMulEquiv_injective, MulEquiv.ofLeftInverse'_symm_apply, Algebra.IsAlgebraic.algEquivEquivAlgHom_apply, Int.subgroup_index_ne_zero_iff, IsCyclic.mulAutMulEquiv_symm_apply_symm_apply, MulEquiv.toAdditive_symm_apply_symm_apply, galRestrictHom_symm_apply, MulEquiv.monoidHomCongrRight_apply, MulEquiv.punitCoprod_apply, CategoryTheory.Iso.self_symm_conj, Units.toAut_inv, Submonoid.LocalizationMap.ofMulEquivOfLocalizations_eq_iff_eq, MonoidAlgebra.mapDomainRingEquiv_apply, nonZeroDivisorsEquivUnits_apply, MulEquiv.toAdditive_apply_symm_apply, CategoryTheory.Iso.conjAut_hom, Submonoid.coe_equivMapOfInjective_apply, Equiv.Perm.equivUnitsEnd_symm_apply_symm_apply, Submonoid.LocalizationMap.mulEquivOfMulEquiv_mk', abelianizationCongr_of, SubMulAction.fixingSubgroupEquivFixingSubgroup_coe_apply, coe_toLexMulEquiv, Algebra.IsAlgebraic.algEquivEquivAlgHom_symm_apply, toUnits_symm_apply, Units.coe_opEquiv_symm, Equiv.permCongrHom_coe_equiv, Matrix.SpecialLinearGroup.toLin_equiv.toLinearMap_eq, MonoidHom.ofInjective_apply, MulEquiv.coe_subgroupMap_apply, rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar_val, MulAutMultiplicative_apply_symm_apply, ModuleCat.Iso.conj_eq_conj, nonZeroDivisorsEquivUnits_symm_apply_coe, Equiv.Perm.cycleFactorsFinset_conj, MulEquiv.toMulHom_eq_coe, WithZero.withZeroUnitsEquiv_symm_apply, CategoryTheory.Iso.conj_id, MulEquiv.coprodCongr_symm_apply, PresentedGroup.equivPresentedGroup_symm_apply_of, CategoryTheory.ActionCategory.stabilizerIsoEnd_apply, MulEquiv.comp_left_injective, SubMulAction.ofFixingSubgroup_of_eq_bijective, IsGaloisGroup.mulEquivAlgEquiv_symm_apply, CategoryTheory.Iso.trans_conj, MulEquiv.funUnique_apply, Equiv.Perm.equivUnitsEnd_symm_apply_apply, rootsOfUnityCircleEquiv_apply, Action.resEquiv_inverse, toUnits_val_apply, SemidirectProduct.inv_left, MulEquiv.coprodAssoc_symm_apply_inl, Subgroup.IsComplement'.QuotientMulEquiv_symm_apply, MulEquiv.symm_comp_eq, MulOpposite.coe_opMulEquiv, uliftZPowersHom_apply_apply, Submonoid.comap_equiv_eq_map_symm, SemidirectProduct.mulEquivSubgroup_apply, Subsemigroup.map_equiv_top, IsCyclic.mulAutMulEquiv_symm_apply_apply, OrderMonoidIso.toMulEquiv_injective, CoxeterSystem.map_simple, MulEquiv.withZero_symm_apply_apply, MulEquiv.op_symm_apply_symm_apply, AddEquiv.toMultiplicativeLeft_symm_apply_apply, CategoryTheory.Iso.conjAut_zpow, Subgroup.mem_iff_toUnits_mem_units, MulAut.conjNormal_inv_apply, Submonoid.map_equiv_top, MulEquiv.bijective, Subgroup.subgroupOfEquivOfLe_apply_coe, SemidirectProduct.mulEquivProd_apply, ConjAct.ofConjAct_mul, mulEquivOfOrderOfEq_apply_gen, MulEquiv.coe_toEquiv, QuotientGroup.quotientBot_apply, CoxeterMatrix.reindexGroupEquiv_symm_apply_simple, AffineEquiv.val_inv_equivUnitsAffineMap_apply, MonoidAlgebra.domCongr_support, Submonoid.leftInvEquiv_symm_fromLeftInv, autEquivRootsOfUnity_apply_rootOfSplit, SpecialLinearGroup.centerEquivRootsOfUnity_apply_apply, AddConstEquiv.equivUnits_symm_apply_symm_apply, SemidirectProduct.mulEquivSubgroup_symm_apply, freeGroupEquivCoprodI_apply, Unitary.conjStarAlgAut_symm_unitaryLinearIsometryEquiv, CategoryTheory.Functor.FullyFaithful.mulEquivEnd_apply, ConjAct.ofConjAct_inv, Action.resEquiv_functor, MulEquiv.coe_toEquiv_symm, ClassGroup.equiv_mk0, MulEquiv.symm_bijective, WithZero.toMulBot_le, MulEquiv.op_symm_apply_apply, MulEquiv.Monoid.End_apply, SubMulAction.ofStabilizer.conjMap_bijective, Submonoid.LocalizationMap.mulEquivOfMulEquiv_eq, SemidirectProduct.mulEquivProd_symm_apply_right, Submonoid.LocalizationMap.symm_comp_ofMulEquivOfLocalizations_apply, MulAut.apply_inv_self, CategoryTheory.Iso.conj_comp, MulEquiv.map_mul, Subgroup.equivSMul_symm_apply_coe, Subgroup.comap_normalClosure, MulEquiv.coprodAssoc_symm_apply_inr_inl, Subgroup.IsComplement'.QuotientMulEquiv_apply, WithZero.withZeroUnitsEquiv_apply, HNNExtension.equiv_symm_eq_conj, FreeGroup.freeGroupCongr_apply, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_coe, Submonoid.topEquiv_toMonoidHom, Action.Iso.conj_ρ, ModularForm.coe_translate, MulEquiv.piCongrRight_apply, SemidirectProduct.mul_left, FreeGroupBasis.map_apply, MulEquiv.subsemigroupMap_apply_coe, MulEquiv.subsemigroupMap_symm_apply_coe, MulEquiv.subgroupMap_symm_apply, Nonneg.val_inv_unitsEquivPos_symm_apply_coe, val_rootsOfUnityEquivOfPrimitiveRoots_apply_coe, FreeMonoid.freeMonoidCongr_symm_of, MulEquiv.coe_toMulHom, ClassGroup.equivPic_apply, Submonoid.val_unitsTypeEquivIsUnitSubmonoid_symm_apply, MonoidHom.toHomUnitsMulEquiv_symm_apply, AddOpposite.opMulEquiv_apply, MulEquiv.val_piUnits_apply, MulEquiv.coe_monoidHom_comp_coe_monoidHom_symm, Equiv.mulEquiv_symm_apply, Equiv.Perm.mem_conj_support, MulEquiv.toSingleObjEquiv_functor_map, addMonoidEndToMultiplicative_apply_apply, MulEquiv.ofBijective_apply, Subgroup.normalizerMonoidHom_apply_symm_apply_coe, galRestrictHom_apply, LinearOrderedCommGroupWithZero.inl_apply, Unitization.val_unitsFstOne_mulEquiv_quasiregular_apply, Con.comap_conGen_equiv, LinearOrderedCommGroupWithZero.inr_apply, MulEquiv.coe_monoidHom_refl, Submonoid.centerCongr_apply_coe, CategoryTheory.Hom.mulEquivCongrRight_apply, Subgroup.centerToMulOpposite_symm_apply_coe, Localization.mulEquivOfQuotient_symm_mk', Submonoid.powLogEquiv_symm_apply, MulEquiv.finite_right, MulEquiv.injective, ConjAct.toConjAct_ofConjAct, FGModuleCat.Iso.conj_hom_eq_conj, MonoidHom.apply_ofInjective_symm, powersMulHom_symm_apply, MulOpposite.opMulEquiv_symm_apply, Subsemigroup.coe_equivMapOfInjective_apply, QuotientGroup.quotientBot_symm_apply, Equiv.Perm.val_inv_equivUnitsEnd_apply, Submonoid.LocalizationMap.symm_comp_ofMulEquivOfLocalizations_apply', Finite.exists_type_univ_nonempty_mulEquiv, ConjAct.toConjAct_one, CategoryTheory.Iso.conjAut_pow, LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv, algebraMap_galRestrictHom_apply, SubMulAction.ofStabilizer.conjMap_apply, Subgroup.topEquiv_apply, MulEquiv.symm_apply_apply, CategoryTheory.Iso.conj_apply, ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk, AddConstEquiv.coe_val_equivUnits_apply, WithZero.toMulBot_symm_bot, CategoryTheory.PreGaloisCategory.endMulEquivAutGalois_pi, rootsOfUnityEquivOfPrimitiveRoots_symm_apply, Units.mapContinuousMulEquiv_apply, MonoidAlgebra.domCongr_apply, StarMulEquiv.coe_toMulEquiv, ValuationSubring.coe_unitGroupToResidueFieldUnits_apply, AddAutAdditive_symm_apply_apply, SubMulAction.ofFixingSubgroup_insert_map_bijective, PresentedGroup.equivPresentedGroup_apply_of, AddAut.congr_apply, ConjAct.ofConjAct_one, Subgroup.map_equiv_eq_comap_symm, Subgroup.IsArithmetic.conj, MulEquiv.subgroupCongr_symm_apply, Submonoid.topEquiv_apply, CategoryTheory.ActionCategory.stabilizerIsoEnd_symm_apply, lipschitzGroup.conjAct_smul_range_ι, WithZero.toMulBot_strictMono, SubMulAction.conjMap_ofFixingSubgroup_bijective, Units.coe_mapEquiv, AffineEquiv.equivUnitsAffineMap_symm_apply_invFun, IsGaloisGroup.map_mulEquivAlgEquiv_fixingSubgroup, IsCyclotomicExtension.autEquivPow_symm_apply, WithZero.unitsWithZeroEquiv_apply, AlgEquiv.algHomUnitsEquiv_apply_apply, IsCusp.smul, Rat.ringOfIntegersWithValEquiv_apply, SpecialLinearGroup.centerEquivRootsOfUnity_apply_of_finrank_le_one, MulEquiv.map_finprod_mem, ClassGroup.equiv_mk, MulEquiv.symmEquiv_apply_symm_apply, ConjAct.smul_eq_mulAut_conj, addMonoidEndToMultiplicative_symm_apply_apply, Matrix.GeneralLinearGroup.toLin_apply, AddEquiv.toMultiplicativeLeft_apply_apply, Subsemigroup.centerCongr_apply_coe, Subsemigroup.comap_equiv_eq_map_symm, ValuationSubring.principalUnitGroup_symm_apply, WithZero.withZeroUnitsEquiv_strictMono, MonoidHom.toMulEquiv_apply, RootPairing.Equiv.toEndUnit_val, MulEquiv.coe_prodComm, Submonoid.LocalizationMap.mulEquivOfMulEquiv_eq_map_apply, Abelianization.equivOfComm_symm_apply, IsCyclotomicExtension.autEquivPow_apply, MulEquiv.refl_apply, SubMulAction.conjMap_ofFixingSubgroup_coe_apply, MulEquiv.val_inv_piUnits_symm_apply, Submodule.unitsQuotEquivRelPic_apply_coe, MonoidHom.toHomUnitsMulEquiv_apply, MulEquiv.apply_symm_apply, QuotientGroup.quotientMulEquivOfEq_mk, CategoryTheory.Iso.commGroupIsoToMulEquiv_apply, IsCyclotomicExtension.Rat.galEquivZMod_smul_of_pow_eq, AddAut.congr_symm_apply, MulEquiv.withZero_symm_apply_symm_apply, MulAut.congr_symm_apply, GrpWithZero.Iso.mk_inv, CategoryTheory.Iso.conjAut_trans, MulEquiv.piMultiplicative_symm_apply, Submonoid.mul_leftInvEquiv_symm, prod_galRestrict_eq_norm, Subgroup.isCoatom_comap, autEquivRootsOfUnity_smul, MulEquiv.inv_apply, MulAut.conjNormal_apply, unitary.linearIsometryEquiv_coe_apply
MulEquivClass 📖	CompData	7 math math: BialgEquivClass.toMulEquivClass, OrderMonoidIso.instMulEquivClass, MulEquiv.instMulEquivClass, RingEquivClass.toMulEquivClass, GroupExtension.Equiv.instMulEquivClass, StarMulEquiv.instMulEquivClass, ContinuousMulEquiv.instMulEquivClass
instCoeTCAddEquivOfAddEquivClass 📖	CompOp	—
instCoeTCMulEquivOfMulEquivClass 📖	CompOp	—
«term_≃*_» 📖	CompOp	—
«term_≃+_» 📖	CompOp	—

---

← Back to Index