| Name | Category | Theorems |
|---|
copy π | CompOp | 3 mathmath: val_copy, val_neg_copy, copy_eq
|
instAdd π | CompOp | 23 mathmath: val_toAddUnits_apply, AddSemiconjBy.addUnits_val_iff, AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid_apply_coe, AddSubmonoid.val_neg_addUnitsTypeEquivIsAddUnitAddSubmonoid_symm_apply, AddEquiv.val_neg_piAddUnits_apply, coe_unop_opEquiv, AddSubgroup.mem_iff_toAddUnits_mem_addUnits, AddCommute.addUnits_of_val, AddSubgroup.mem_ofAddUnits_iff_toAddUnits_mem, instContinuousAdd, AddCommute.addUnits_val_iff, AddSubmonoid.val_addUnitsTypeEquivIsAddUnitAddSubmonoid_symm_apply, IsAddUnit.addUnit_add, val_add, AddEquiv.val_piAddUnits_symm_apply, Set.subset_addCenter_add_units, AddSemiconjBy.addUnits_of_val, AddEquiv.val_neg_piAddUnits_symm_apply, toAddUnits_symm_apply, coe_opEquiv_symm, AddSubmonoid.add_mem_addUnits, toAddUnits_val_apply, AddEquiv.val_piAddUnits_apply
|
instAddCommGroupAddUnits π | CompOp | 2 mathmath: instAddArchimedean, isOrderedAddMonoid
|
instAddGroup π | CompOp | 37 mathmath: AddSubgroup.ofAddUnits_right_inverse, AddSubgroup.ofAddUnits_bot, ofAddUnits_addUnits_gc, AddSubmonoid.addUnits_iInfβ, AddSubmonoid.addUnits_sInf, AddSubgroup.mem_iff_toAddUnits_mem_addUnits, ofAddUnits_le_iff_le_addUnits, AddSubmonoid.addUnits_iInf, AddSubmonoid.neg_mem_addUnits_iff, AddSubgroup.mem_ofAddUnits_iff_toAddUnits_mem, AddSubmonoid.addUnits_mono, AddSubmonoid.addUnits_bot, AddSubgroup.ofAddUnits_injective, AddSubgroup.ofAddUnits_sSup, AddSubgroup.addUnit_of_mem_ofAddUnits_spec_mem, AddSubgroup.ofAddUnits_inf, AddSubgroup.ofAddUnits_mono, AddSubmonoid.addUnits_inf, AddSubgroup.mem_ofAddUnits_iff_exists_isAddUnit, AddSubmonoid.mem_addUnits_of_val_mem_neg_val_mem, AddSubgroup.ofAddUnits_iSupβ, AddSubgroup.mem_of_mem_val_ofAddUnits, AddSubgroup.ofAddUnits_inf_addUnits, AddSubgroup.addUnit_mem_of_mem_ofAddUnits, AddSubmonoid.isOpen_addUnits, instIsTopologicalAddGroupOfContinuousAdd, AddSubgroup.ofAddUnits_strictMono, AddSubgroup.val_mem_ofAddUnits_iff_mem, AddSubmonoid.addUnits_left_inverse, AddSubgroup.ofAddUnits_sup_addUnits, AddSubgroup.mem_addUnits_iff_val_mem, AddSubmonoid.mem_addUnits_iff, AddSubgroup.mem_ofAddUnits_iff, AddSubgroup.ofAddUnits_iSup, AddSubmonoid.addUnits_surjective, AddSubmonoid.addUnits_top, AddSubgroup.exists_mem_ofAddUnits_val_eq
|
instAddMonoid π | CompOp | 6 mathmath: IsAddUnit.addUnit_nsmul, isOfFinAddOrder_val, addOrderOf_addUnits, val_nsmul_eq_nsmul_val, neg_nsmul_eq_nsmul_neg, nsmul_ofNSMulEqZero
|
instAddZeroClass π | CompOp | 37 mathmath: map_mk, AddSubmonoid.LocalizationMap.add_neg_right, embedProduct_injective, coeHom_apply, IsAddUnit.add_liftRight_neg, AddSubmonoid.mk_add_mk_neg_eq_zero, Continuous.addUnits_map, AddSubmonoid.LocalizationMap.lift_apply, AddMonoidHom.ker_toHomAddUnits, add_liftRight_neg, AddSubmonoid.LocalizationMap.add_neg, liftRight_neg_add, AddSubmonoid.LocalizationMap.neg_unique, coeHom_injective, map_bijective, AddMonoidHom.coe_toHomAddUnits, embedProduct_apply, AddSubmonoid.mk_neg_add_mk_eq_zero, coe_map_neg, coe_map, map_injective, range_embedProduct, IsAddUnit.coe_liftRight, isOpenMap_map, map_id, IsAddUnit.liftRight_neg_add, coe_liftRight, AddSubmonoid.LocalizationMap.lift_mk', continuous_embedProduct, continuous_map, isClosedEmbedding_embedProduct, isEmbedding_embedProduct, isInducing_embedProduct, map_comp, val_addUnitsCenterToCenterAddUnits_apply_coe, addUnitsCenterToCenterAddUnits_injective, AddSubmonoid.LocalizationMap.add_neg_left
|
instCoeHead π | CompOp | β |
instDecidableEq π | CompOp | β |
instInhabited π | CompOp | β |
instNeg π | CompOp | 94 mathmath: AddSubmonoid.coe_val_add_coe_neg_val, AddSubmonoid.LocalizationMap.add_neg_right, AddSubmonoid.addUnit_mem_leftNeg, addCommute_iff_neg_add_cancel_assoc, IsAddUnit.add_val_neg, AddSubmonoid.val_neg_addUnitsTypeEquivIsAddUnitAddSubmonoid_symm_apply, AddEquiv.val_neg_piAddUnits_apply, AddSemiconjBy.addUnits_neg_right, neg_eq_of_add_eq_zero_left, add_neg_eq_add_neg_iff, IsAddUnit.add_liftRight_neg, val_neg_mulLeft, neg_add, eq_neg_of_add_eq_zero_right, addCommute_coe_neg, AddSubmonoid.neg_mem_addUnits_iff, val_neg_mulRight, eq_neg_of_add_eq_zero_left, AddSemiconjBy.addUnits_neg_symm_left_iff, AddSubmonoid.neg_val_mem_of_mem_addUnits, Set.addUnits_neg_mem_center, AddSemiconjBy.addUnits_neg_right_iff, neg_add_of_eq, IsAddUnit.addUnit_neg, IsAddUnit.val_neg_apply, addLeft_symm, add_eq_zero_iff_neg_eq, neg_eq_of_add_eq_zero_right, ContinuousMap.addUnitsLift_apply_neg_apply, neg_mul_right, add_neg_of_eq, neg_mulRight, AddSubmonoid.LocalizationMap.lift_apply, IsOfFinAddOrder.val_neg_addUnit, AddCommute.addUnits_neg_left_iff, neg_eq_val_neg, AddSubmonoid.coe_neg_val_add_coe_val, add_liftRight_neg, val_neg_inj, AddSubmonoid.LocalizationMap.add_neg, addCommute_iff_add_neg_cancel_assoc, liftRight_neg_add, IsAddUnit.val_neg_add, AddSubmonoid.LocalizationMap.neg_unique, addRight_symm, add_neg_cancel_left, addCommute_iff_neg_add_cancel, add_neg_cancel_right, add_neg, embedProduct_apply, neg_mulLeft, neg_add_eq_zero, coe_map_neg, neg_mk, add_neg_eq_iff_eq_add, IsAddUnit.addUnit_neg_map, neg_add_cancel_right, add_eq_zero_iff_eq_neg, neg_add_eq_neg_add_iff, eq_add_neg_iff_add_eq, AddOreLocalization.universalAddHom_apply, AddSubmonoid.neg_mem_addUnits, neg_unique, AddCommute.addUnits_neg_left, AddCommute.addUnits_neg_right_iff, vadd_neg, AddSubmonoid.IsUnit.Submonoid.coe_neg, AddEquiv.val_neg_piAddUnits_symm_apply, neg_add_eq_iff_eq_add, mk_addSemiconjBy, IsAddUnit.liftRight_neg_add, AddSubmonoid.mem_addUnits_iff, neg_add_cancel_left, neg_mul_eq_mul_neg, map_addUnits_neg, IsAddUnit.neg_vadd, AddSubmonoid.LocalizationMap.lift_mk', neg_nsmul_eq_nsmul_neg, val_neg_eq_neg_val, neg_mul_neg, addCommute_iff_add_neg_cancel, neg_mul_left, val_neg_ofNSMulEqZero, ContinuousMap.addUnitsLift_symm_apply_apply_neg', topology_eq_inf, eq_neg_add_iff_add_eq, IsAddUnit.val_neg_addUnit', AddSemiconjBy.addUnits_neg_symm_left, addCommute_neg_coe, AddSubmonoid.LocalizationMap.add_neg_left, AddCommute.addUnits_neg_right, continuous_iff, continuous_coe_neg, add_neg_eq_zero
|
instRepr π | CompOp | β |
instSub π | CompOp | 2 mathmath: IsAddUnit.addUnit_sub, val_sub_eq_sub_val
|
instSubNegAddMonoid π | CompOp | 4 mathmath: AddCommute.addUnits_zsmul_right, AddSemiconjBy.addUnits_zsmul_right, AddCommute.addUnits_zsmul_left, val_zsmul_eq_zsmul_val
|
instZero π | CompOp | 6 mathmath: Nat.addUnits_eq_zero, val_zero, eq_zero, val_eq_zero, IsAddUnit.addUnit_zero, nsmul_ofNSMulEqZero
|
mkOfAddEqZero π | CompOp | 1 mathmath: val_mkOfAddEqZero
|
neg π | CompOp | 7 mathmath: val_neg, AddEquiv.val_neg_piAddUnits_apply, val_neg_mulLeft, val_neg_mulRight, neg_eq_val_neg, neg_val, AddEquiv.val_neg_piAddUnits_symm_apply
|
val π | CompOp | 139 mathmath: val_toAddUnits_apply, orderEmbeddingVal_apply, AddSemiconjBy.addUnits_val_iff, vadd_def, AddSubmonoid.coe_val_add_coe_neg_val, AddSubmonoid.LocalizationMap.add_neg_right, addLeft_bijective, isOfFinAddOrder_val, AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid_apply_coe, addCommute_iff_neg_add_cancel_assoc, IsAddUnit.add_val_neg, val_neg, AddSubmonoid.val_neg_addUnitsTypeEquivIsAddUnitAddSubmonoid_symm_apply, AddEquiv.val_neg_piAddUnits_apply, AddSemiconjBy.addUnits_val, coeHom_apply, add_neg_eq_add_neg_iff, coe_unop_opEquiv, addOrderOf_addUnits, IsAddUnit.add_liftRight_neg, addRight_bijective, val_injective, val_neg_mulLeft, neg_add, addCommute_coe_neg, isAddUnit_add_addUnits, val_neg_mulRight, AddSemiconjBy.addUnits_neg_symm_left_iff, AddSubmonoid.neg_val_mem_of_mem_addUnits, AddSemiconjBy.addUnits_neg_right_iff, instCanLiftAddUnitsValIsAddUnit, val_zero, AddCommute.addUnits_val_iff, val_sub_eq_sub_val, val_mulLeft, IsAddUnit.val_neg_apply, continuous_val, add_eq_zero_iff_neg_eq, ContinuousMap.addUnitsLift_apply_neg_apply, val_vadd, AddSubmonoid.LocalizationMap.lift_apply, addRight_apply, AddSubmonoid.val_addUnitsTypeEquivIsAddUnitAddSubmonoid_symm_apply, IsOfFinAddOrder.val_neg_addUnit, isAddUnit, AddCommute.addUnits_neg_left_iff, val_nsmul_eq_nsmul_val, isAddUnit_addUnits_add, neg_eq_val_neg, AddSubmonoid.coe_neg_val_add_coe_val, val_inj, ContinuousMap.val_addUnitsLift_apply_apply, val_neg_inj, AddSubmonoid.LocalizationMap.add_neg, addCommute_iff_add_neg_cancel_assoc, IsAddUnit.addUnit_spec, IsAddUnit.val_neg_add, AddSubmonoid.LocalizationMap.neg_unique, val_eq_zero, AddMonoidHom.coe_toHomAddUnits, add_neg_cancel_left, add_left_inj, addCommute_iff_neg_add_cancel, add_neg_cancel_right, add_neg, isEmbedding_val, IsOfFinAddOrder.val_addUnit, IsAddUnit.addUnit_map, embedProduct_apply, neg_add_eq_zero, coe_map_neg, ext_iff, coe_map, neg_val, val_mulRight, add_neg_eq_iff_eq_add, ContinuousMap.val_addUnitsLift_symm_apply_apply, IsAddUnit.addUnit_neg_map, val_le_val, val_ofNSMulEqZero, neg_add_cancel_right, val_add, isAddRegular, add_eq_zero_iff_eq_neg, AddEquiv.val_piAddUnits_symm_apply, IsAddUnit.coe_liftRight, neg_add_eq_neg_add_iff, AddSubgroup.val_mem_ofAddUnits_iff_mem, eq_add_neg_iff_add_eq, Set.subset_addCenter_add_units, addIrreducible_add_addUnits, AddSubgroup.mem_addUnits_iff_val_mem, embedding_val_mk, AddCommute.addUnits_neg_right_iff, add_right_inj, AddSubmonoid.IsUnit.Submonoid.coe_neg, AddCommute.addUnits_val, AddEquiv.val_neg_piAddUnits_symm_apply, neg_add_eq_iff_eq_add, mk_addSemiconjBy, IsAddUnit.liftRight_neg_add, val_mkOfAddEqZero, AddSubmonoid.mem_addUnits_iff, neg_add_cancel_left, AddSubgroup.addUnit_of_mem_ofAddUnits_spec_val_eq_of_mem, neg_mul_eq_mul_neg, map_addUnits_neg, toAddUnits_symm_apply, val_lt_val, AddSubgroup.mem_ofAddUnits_iff, coe_opEquiv_symm, AddSubmonoid.LocalizationMap.lift_mk', neg_nsmul_eq_nsmul_neg, val_neg_eq_neg_val, neg_mul_neg, addCommute_iff_add_neg_cancel, IsAddUnit.val_addUnit', toAddUnits_val_apply, addLeft_apply, AddSubmonoid.val_mem_of_mem_addUnits, addIrreducible_addUnits_add, val_zsmul_eq_zsmul_val, val_neg_ofNSMulEqZero, ContinuousMap.addUnitsLift_symm_apply_apply_neg', val_mk, AddEquiv.val_piAddUnits_apply, topology_eq_inf, eq_neg_add_iff_add_eq, IsAddUnit.val_neg_addUnit', val_addUnitsCenterToCenterAddUnits_apply_coe, min_val, addCommute_neg_coe, AddSubmonoid.LocalizationMap.add_neg_left, continuous_iff, AddSubgroup.exists_mem_ofAddUnits_val_eq, continuous_coe_neg, compare_val, max_val, add_neg_eq_zero
|
| Name | Category | Theorems |
|---|
copy π | CompOp | 3 mathmath: copy_eq, val_inv_copy, val_copy
|
instCoeHead π | CompOp | β |
instCommGroupUnits π | CompOp | 63 mathmath: ComplexShape.eulerCharSignsDownNat_Ο, toMul_uzpow, CommGroup.monoidHom_mulEquiv_of_hasEnoughRootsOfUnity, ker_zpowGroupHom_eq_rootsOfUnity, uzpow_natCast, Complex.isQuotientCoveringMap_npow, uzpow_coe_nat, Equiv.Perm.sign_eq_prod_prod_Ioi, isPrimitiveRoot_of_mem_rootsOfUnity, ComplexShape.Ξ΅_down_β, coe_prod, NumberField.Units.logEmbeddingQuot_apply, NumberField.Units.instFiniteIntAdditiveUnitsRingOfIntegers, IsDedekindDomain.selmerGroup.monotone, Module.Basis.det_unitsSMul, CommMonCat.val_units_map_hom_apply, CommMonCat.val_inv_units_map_hom_apply, isQuotientCoveringMap_npow, NumberField.Units.fundSystem_mk, Equiv.Perm.sign_eq_prod_prod_Iio, NumberField.InfinitePlace.ComplexEmbedding.conjugate_sign, NumberField.Units.rank_modTorsion, IsPrimitiveRoot.coe_units_iff, IsCyclic.monoidHom_equiv_self, Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator, MonoidHom.toHomUnits_mul, groupCohomology.norm_ofAlgebraAutOnUnits_eq, rootsOfUnity_eq_ker, Int.negOnePow_def, Submodule.unitsQuotEquivRelPic_symm_apply, IsPrimitiveRoot.isUnit_unit', isQuotientCoveringMap_zpow, ClassGroup.equivPic_symm_apply, IsDedekindDomain.selmerGroup.fromUnit_ker, ComplexShape.eulerCharSignsUpNat_Ο, ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply, IsDedekindDomain.selmerGroup.fromUnitLift_injective, NumberField.Units.logEmbeddingQuot_injective, IsPrimitiveRoot.isUnit_unit, uzpow_intCast, instMulArchimedean, Module.Basis.orientation_unitsSMul, NumberField.Units.logEmbeddingEquiv_apply, NumberField.Units.exist_unique_eq_mul_prod, MonoidHom.restrict_surjective, Equiv.Perm.sign_prodCongrRight, NumberField.Units.instFiniteIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion, mk0_prod, Equiv.Perm.sign_prodCongrLeft, IsDedekindDomain.HeightOneSpectrum.valuation_of_unit_mod_eq, MonoidHom.toHomUnitsMulEquiv_symm_apply, mulArchimedean_iff, Equiv.Perm.sign_of_cycleType', NumberField.IsCMField.map_unitsMulComplexConjInv_torsion, isOrderedMonoid, ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk, FiniteField.prod_univ_units_id_eq_neg_one, IsDedekindDomain.selmerGroup.valuation_ker_eq, NumberField.Units.instFreeIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion, Submodule.unitsQuotEquivRelPic_apply_coe, MonoidHom.toHomUnitsMulEquiv_apply, Equiv.Perm.OnCycleFactors.sign_kerParam_apply_apply, ofMul_uzpow
|
instDecidableEq π | CompOp | 1 mathmath: UnitsInt.univ
|
instDiv π | CompOp | 6 mathmath: IsUnit.unit_div, Int.units_div_eq_mul, val_div_eq_div_val, uzpow_sub, inv_eq_one_divp', val_div_eq_divp
|
instDivInvMonoid π | CompOp | 64 mathmath: LaurentPolynomial.smeval_eq_sum, Commute.units_zpow_right, ZMod.isCyclic_units_iff_of_odd, CongruenceSubgroup.exists_Gamma_le_conj', ZMod.isCyclic_units_two_mul_iff_of_odd, rootsOfUnity.integer_power_of_ringEquiv, LaurentPolynomial.smeval_T_pow, ZMod.isCyclic_units_one, ZMod.isCyclic_units_iff, IsCusp.of_isFiniteRelIndex_conj, LaurentPolynomial.evalβ_C_mul_T, SlashInvariantForm.coe_translate, ZMod.not_isCyclic_units_of_mul_coprime, instIsCyclicUnitsWithZero, lipschitzGroup.conjAct_smul_ΞΉ_mem_range_ΞΉ, spinGroup.units_involute_act_eq_conjAct, spinGroup.conjAct_smul_ΞΉ_mem_range_ΞΉ, LaurentPolynomial.evalβ_T, spinGroup.conjAct_smul_range_ΞΉ, CongruenceSubgroup.IsArithmetic.conj, ConjAct.units_smul_def, CongruenceSubgroup.isArithmetic_conj_SL2Z, val_zpow_eq_zpow_val, pinGroup.conjAct_smul_ΞΉ_mem_range_ΞΉ, instIsCyclicUnitsOfFinite, CuspForm.coe_translate, cfc_comp_zpow, Unitary.toAlgEquiv_conjStarAlgAut, Commute.units_zpow_left, ZMod.isCyclic_units_of_prime_pow, pinGroup.conjAct_smul_range_ΞΉ, cfc_zpow, val_unitsCentralizerEquiv_symm_apply_coe, isQuotientCoveringMap_zpow, CircleDeg1Lift.translate_zpow, Unitary.toRingEquiv_conjStarAlgAut, ZMod.isCyclic_units_four, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_zpow', LaurentPolynomial.smeval_single, CFC.rpow_intCast, CategoryTheory.CatCenter.app_neg_one_zpow, NumberField.Units.coe_zpow, ZMod.not_isCyclic_units_eight, rootsOfUnity.integer_power_of_ringEquiv', LaurentPolynomial.smeval_C_mul_T_n, ZMod.isCyclic_units_two, NumberField.Units.exist_unique_eq_mul_prod, SemiconjBy.units_zpow_right, ZMod.isCyclic_units_two_pow_iff, ZMod.isCyclic_units_zero, ModularForm.coe_translate, ZMod.isCyclic_units_prime, CategoryTheory.CommShiftβSetup.int_Ξ΅, ZMod.isCyclic_units_four_mul_iff, IsPrimitiveRoot.zmodEquivZPowers_apply_coe_int, Matrix.coe_units_zpow, modularCyclotomicCharacter.aux_spec, Subgroup.IsArithmetic.conj, lipschitzGroup.conjAct_smul_range_ΞΉ, CircleDeg1Lift.translationNumber_zpow, IsCusp.smul, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_zpow, cfcUnits_zpow, CategoryTheory.CommShiftβSetup.int_z
|
instGroup π | CompOp | 404 mathmath: units_inv_smul, Submonoid.units_iInf, ModularGroup.SLOnGLPos_smul_apply, MonoidWithZeroHom.mem_valueGroup, mem_rootsOfUnity, Matrix.GLPos.coe_neg_apply, Subgroup.ofUnits_bot, ValuationSubring.coe_mem_principalUnitGroup_iff, Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_apply, Subgroup.adjoinNegOne_eq_self_iff, modularCyclotomicCharacter.id, rootsOfUnityEquivOfPrimitiveRoots_apply_coe_inv_val, Subgroup.instHasDetOneRangeSpecialLinearGroupGeneralLinearGroupMapGL, NumberField.Units.instNonemptySubtypeUnitsRingOfIntegersMemSubgroupTorsion, autAdjoinRootXPowSubCEquiv_root, ZMod.rootsOfUnity_eq_top, NumberField.IsCMField.unitsComplexConj_torsion, Subgroup.instHasDetOneMapSpecialLinearGroupGeneralLinearGroupToGL, ClassGroup.Quot_mk_eq_mk, WeierstrassCurve.Projective.nonsingularLift_some, Matrix.SpecialLinearGroup.toGLPos_injective, val_inv_unitarySubgroupUnitsEquiv_symm_apply_coe, Valuation.IsRankOneDiscrete.exists_generator_lt_one', Module.Ray.neg_units_smul, Matrix.GeneralLinearGroup.mem_center_iff_val_mem_range_scalar, CongruenceSubgroup.exists_Gamma_le_conj', NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm_apply_fst, ofUnits_le_iff_le_units, Set.unit_eq, SlashInvariantForm.quotientFunc_mk, cyclotomicCharacter.toZModPow, Submonoid.inv_mem_units_iff, Valuation.IsRankOneDiscrete.generator_mem_valueGroup, Set.unitEquivUnitsInteger_symm_apply_coe, val_unitarySubgroupUnitsEquiv_symm_apply_coe, ker_zpowGroupHom_eq_rootsOfUnity, Module.Ray.units_smul_of_neg, IsPrimitiveRoot.val_toRootsOfUnity_coe, Complex.isQuotientCoveringMap_npow, Subgroup.mem_ofUnits_iff_exists_isUnit, rootsOfUnity.integer_power_of_ringEquiv, mem_principal_ideals_iff, Submonoid.units_bot, subgroup_units_cyclic, CongruenceSubgroup.strictPeriods_Gamma0, Subgroup.ofUnits_strictMono, rootsOfUnity.isCyclic, ModularForm.norm_eq_zero_iff, Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_symm_apply_coe_coe, autAdjoinRootXPowSubCEquiv_symm_smul, IsCyclic.monoidHom_mulEquiv_rootsOfUnity, WeierstrassCurve.Projective.Point.zero_point, ModularGroup.coe_apply_complex, Submodule.ker_unitsToPic, ModularForm.levelOne_neg_weight_rank_zero, Subgroup.IsArithmetic.is_commensurable, Subgroup.IsArithmetic.inter, Matrix.GeneralLinearGroup.center_eq_range_scalar, mem_rootsOfUnity_prime_pow_mul_iff', val_unitsCentralizerEquiv_apply_coe, Subgroup.instHasDetOneMinGeneralLinearGroup_1, SpecialLinearGroup.centerCongr_toLin_equiv_trans_centerEquivRootsOfUnity_eq, Complex.mem_rootsOfUnity, CuspForm.coe_trace, Ideal.rootsOfUnityMapQuot_injective, index_posSubgroup, mem_rootsOfUnity_iff_mem_nthRoots, CongruenceSubgroup.exists_Gamma_le_conj, rootsOfUnity.coe_injective, WeierstrassCurve.Projective.addMap_of_Z_eq_zero_left, spinGroup.units_mem_lipschitzGroup, WeierstrassCurve.Jacobian.Point.fromAffine_some, disjoint_rootsOfUnity_of_coprime, Subgroup.instIsArithmeticRangeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGL, Subgroup.mem_adjoinNegOne_iff, NumberField.mixedEmbedding.fundamentalCone.integerSetQuotEquivAssociates_apply, Valuation.IsUniformizer.zpowers_eq_valueGroup, Subgroup.instIsArithmeticMapSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGLOfFiniteIndex, SlashInvariantForm.coe_translate, Subgroup.mem_ofUnits_iff, Subgroup.ofUnits_le_ofUnits_iff, Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, rootsOfUnity_one, HasEnoughRootsOfUnity.natCard_rootsOfUnity, isCusp_SL2Z_iff', instIsTopologicalGroupOfContinuousMul, NumberField.mixedEmbedding.fundamentalCone.integerSetEquiv_apply_fst, WeierstrassCurve.Jacobian.negMap_of_Z_ne_zero, rootsOfUnity.val_mkOfPowEq_coe, NumberField.Units.map_complexEmbedding_torsion, unitarySubgroupUnitsEquiv_apply_coe, NumberField.Units.span_basisOfIsMaxRank, MulEquiv.restrictRootsOfUnity_symm, WeierstrassCurve.Jacobian.nonsingularLift_iff, IsPrimitiveRoot.coe_autToPow_apply, NumberField.Units.logEmbeddingQuot_apply, Subgroup.exists_mem_ofUnits_val_eq, Subgroup.mem_of_mem_val_ofUnits, NumberField.mixedEmbedding.fundamentalCone.integerSetTorsionSMul_smul_coe, Subgroup.commensurable_adjoinNegOne_self, units_smul_eq_self_iff, Set.coe_unit, units_smul_eq_neg_iff, IsDedekindDomain.selmerGroup.monotone, Valuation.mem_unitGroup_iff, Subgroup.strictWidthInfty_eq_one_of_T_mem, HasEnoughRootsOfUnity.rootsOfUnity_isCyclic, MonoidWithZeroHom.valueMonoid_eq_valueGroup, IsPrimitiveRoot.card_rootsOfUnity', Subgroup.negOne_mem_adjoinNegOne, val_set_image_rootsOfUnity_one, FiniteField.sum_subgroup_units_eq_zero, ModularGroup.SL_to_GL_tower, WeierstrassCurve.Projective.smul_eq, ModularFormClass.one_mem_strictPeriods_SL2Z, ValuationSubring.principalUnitGroup_le_principalUnitGroup, MonoidWithZeroHom.valueGroup_eq_range, Valuation.IsRankOneDiscrete.instIsCyclicSubtypeUnitsMemSubgroupValueGroup, ModularForm.levelOne_weight_zero_rank_one, CongruenceSubgroup.strictWidthInfty_Gamma0, modularCyclotomicCharacter.toFun_spec, WeierstrassCurve.Jacobian.negMap_of_Z_eq_zero, CongruenceSubgroup.IsArithmetic.conj, isQuotientCoveringMap_npow, MulChar.apply_mem_rootsOfUnity_of_pow_eq_one, NumberField.Units.fundSystem_mk, MulEquiv.restrictRootsOfUnity_coe_apply, NumberField.IsCMField.indexRealUnits_mul_eq, NumberField.Units.dirichletUnitTheorem.map_logEmbedding_sup_torsion, IsPrimitiveRoot.card_rootsOfUnity, HasEnoughRootsOfUnity.cyc, NumberField.mixedEmbedding.fundamentalCone.unit_smul_mem_iff_mem_torsion, ValuationSubring.coe_unitGroupMulEquiv_apply, NumberField.mixedEmbedding.fundamentalCone.integerSetTorsionSMul_stabilizer, Subgroup.IsArithmetic.isFiniteRelIndexSL, NumberField.Units.rank_modTorsion, ValuationSubring.unitGroup_injective, val_set_image_rootsOfUnity, PrincipalIdeals.normal, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_pow', instLieGroupModelWithCornersSelf, Subgroup.strictPeriods_eq_zmultiples_one_of_T_mem, WeierstrassCurve.Jacobian.nonsingularLift_some, ValuationSubring.mem_unitGroup_iff, CongruenceSubgroup.isArithmetic_conj_SL2Z, Module.Ray.units_smul_of_pos, Orientation.map_eq_det_inv_smul, EisensteinSeries.q_expansion_riemannZeta, NumberField.IsCMField.unitsMulComplexConjInv_apply_torsion, Submonoid.units_isCompact, SpecialLinearGroup.centerEquivRootsOfUnity_symm_apply, mem_posSubgroup, Submonoid.units_top, Unitization.val_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, NumberField.mixedEmbedding.fundamentalCone.quotIntNorm_apply, instIsFiniteRelIndexGeneralLinearGroupAdjoinNegOne, NumberField.Units.mem_torsion, Submonoid.isOpen_units, Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, map_rootsOfUnity_eq_pow_self, Submonoid.units_sInf, WeierstrassCurve.Projective.addMap_eq, Subgroup.val_centerUnitsEquivUnitsCenter_symm_apply_coe, NumberField.Units.regOfFamily_div_regulator, WeierstrassCurve.Jacobian.addMap_of_Z_ne_zero, rootsOfUnity_eq_ker, Valuation.IsRankOneDiscrete.generator_zpowers_eq_range, CuspForm.coe_translate, AddChar.val_mem_rootsOfUnity, NumberField.IsCMField.closure_realFundSystem_sup_torsion, bijective_rootsOfUnityAddChar, NumberField.Units.instIsCyclicSubtypeUnitsRingOfIntegersMemSubgroupTorsion, WeierstrassCurve.Jacobian.addMap_of_Z_eq_zero_right, Submonoid.units_surjective, Set.val_unitEquivUnitsInteger_apply_coe, Submonoid.units_left_inverse, Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_apply, Subgroup.mem_ofUnits_iff_toUnits_mem, rootsOfUnity.coe_mkOfPowEq, ValuationSubring.unitGroup_strictMono, Subgroup.isArithmetic_iff_finiteIndex, Subgroup.ofUnits_inf, NumberField.Units.closure_fundSystem_sup_torsion_eq_top, EisensteinSeries.isBoundedAtImInfty_eisensteinSeries_SIF, Submodule.range_unitsToPic, ofUnits_units_gc, Unitary.toAlgEquiv_conjStarAlgAut, Subgroup.instHasDetOneMinGeneralLinearGroup, isCusp_SL2Z_iff, pinGroup.units_mem_iff, WeierstrassCurve.Projective.Point.fromAffine_some, NumberField.Units.torsion_eq_one_or_neg_one_of_odd_finrank, surjective_rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar, surjective_cosetToCuspOrbit, WeierstrassCurve.Projective.negMap_of_Z_ne_zero, CongruenceSubgroup.strictWidthInfty_Gamma1, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_pow, WeierstrassCurve.Projective.nonsingularLift_iff, Module.stabilizer_units_eq_bot_of_ne_zero, HahnSeries.binomial_power, EisensteinSeries.eisensteinSeries_SIF_apply, Submonoid.units_inf, NumberField.Units.dirichletUnitTheorem.logEmbedding_eq_zero_iff, val_unitsCentralizerEquiv_symm_apply_coe, Submodule.unitsQuotEquivRelPic_symm_apply, Subgroup.ofUnits_mono, Subgroup.ofUnits_inf_units, Subgroup.val_centerUnitsEquivUnitsCenter_apply_coe, WeierstrassCurve.Jacobian.nonsingularLift_zero, Matrix.SpecialLinearGroup.coe_GLPos_neg, isQuotientCoveringMap_zpow, WeierstrassCurve.Projective.addMap_of_Y_eq, HahnSeries.pow_add, NumberField.IsCMField.unitsMulComplexConjInv_ker, Unitary.toRingEquiv_conjStarAlgAut, ValuationSubring.unitGroup_le_unitGroup, ValuationSubring.principal_units_le_units, rootsOfUnity_inf_rootsOfUnity, Valuation.IsRankOneDiscrete.generator_zpowers_eq_valueGroup, WeierstrassCurve.Projective.negMap_eq, pinGroup.units_mem_lipschitzGroup, Matrix.GeneralLinearGroup.mem_center_iff_val_eq_scalar, SpecialLinearGroup.centerEquivRootsOfUnity_apply, NumberField.IsCMField.unitsMulComplexConjInv_apply, Set.unit_valuation_eq_one, CongruenceSubgroup.strictPeriods_Gamma1, pinGroup.mem_lipschitzGroup, NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociates_eq_iff, SlashInvariantForm.coe_trace, WeierstrassCurve.Jacobian.addMap_of_Z_eq_zero_left, ClassGroup.equivPic_symm_apply, NumberField.IsCMField.mem_realUnits_iff, WeierstrassCurve.Projective.addMap_of_Z_eq_zero_right, CongruenceSubgroup.strictWidthInfty_Gamma, NumberField.IsCMField.unitsComplexConj_eq_self_iff, ValuationSubring.surjective_unitGroupToResidueFieldUnits, EisensteinSeries.q_expansion_bernoulli, ValuationSubring.principalUnitGroupEquiv_apply, MonCat.val_units_map_hom_apply, Submonoid.mem_units_iff, IsDedekindDomain.selmerGroup.fromUnit_ker, Matrix.GeneralLinearGroup.center_eq_range_units, Subgroup.unit_mem_of_mem_ofUnits, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_zpow', Valuation.instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial, Matrix.SpecialLinearGroup.eq_scalar_center_equiv_rootsOfUnity, MonoidWithZeroHom.valueGroup_def, Matrix.SpecialLinearGroup.coe_to_GLPos_to_GL_det, val_set_image_rootsOfUnity_two, ValuationSubring.mem_principalUnitGroup_iff, Module.Basis.map_orientation_eq_det_inv_smul, CongruenceSubgroup.strictPeriods_Gamma, cosetToCuspOrbit_apply_mk, ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply, IsDedekindDomain.selmerGroup.fromUnitLift_injective, LinearEquiv.smulOfNeZero_symm_apply, NumberField.Units.logEmbeddingQuot_injective, WeierstrassCurve.Projective.Point.zero_def, cyclotomicCharacter.toZModPow_toFun, ValuationSubring.coe_unitGroupMulEquiv_symm_apply, MonoidWithZeroHom.valueMonoid_eq_valueGroup', Matrix.mem_glpos, Subgroup.le_adjoinNegOne, Ideal.torsionMapQuot_injective, pinGroup.mem_iff, ModularGroup.coe_one, IsPrimitiveRoot.zpowers_eq, IsCyclic.mulAutMulEquiv_symm_apply_symm_apply, ModularForm.coe_norm, Subgroup.strictPeriods_SL2Z, WeierstrassCurve.Projective.negMap_of_Z_eq_zero, modularCyclotomicCharacter.comp, WeierstrassCurve.Projective.addMap_of_Z_ne_zero, AddAut.mulLeft_apply_apply, lipschitzGroup.coe_mem_iff_mem, Subgroup.mem_strictPeriods_iff, MonoidWithZeroHom.mem_valueGroup_iff_of_comm, MonCat.val_inv_units_map_hom_apply, Submonoid.units_iInfβ, rootsOfUnity_le_of_dvd, Subgroup.val_mem_ofUnits_iff_mem, Matrix.SpecialLinearGroup.coe_GLPos_coe_GL_coe_matrix, rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar_val, SlashInvariantForm.vAdd_width_periodic, WeierstrassCurve.Jacobian.Point.zero_point, rootsOfUnityEquivNthRoots_apply, Subgroup.ofUnits_injective, NumberField.IsCMField.indexRealUnits_eq_two_iff, card_rootsOfUnity_eq_iff_exists_isPrimitiveRoot, rootsOfUnityCircleEquiv_apply, Module.Basis.orientation_unitsSMul, Complex.card_rootsOfUnity, Subgroup.ofUnits_iSupβ, EisensteinSeries.eisensteinSeriesSIF_apply, IsCyclic.mulAutMulEquiv_symm_apply_apply, Module.End.mulSemiringActionToAlgEquiv_conjAct_surjective, DirichletCharacter.factorsThrough_iff_ker_unitsMap, IsPrimitiveRoot.mem_rootsOfUnity, WeierstrassCurve.Jacobian.Point.zero_def, NumberField.Units.logEmbeddingEquiv_apply, Subgroup.mem_iff_toUnits_mem_units, NumberField.Units.isMaxRank_iff_closure_finiteIndex, NumberField.Units.exist_unique_eq_mul_prod, Subgroup.unit_of_mem_ofUnits_spec_mem, EisensteinSeries.eisensteinSeries_tendstoLocallyUniformlyOn, NumberField.Units.rootsOfUnity_eq_one, orbitRel_nonZero_iff, autEquivRootsOfUnity_apply_rootOfSplit, HahnSeries.coeff_toOrderTopSubOnePos_pow, SpecialLinearGroup.centerEquivRootsOfUnity_apply_apply, rootsOfUnity.coe_pow, restrictRootsOfUnity_coe_apply, Subgroup.ofUnits_sSup, IsPrimitiveRoot.zmodEquivZPowers_apply_coe_nat, HasEnoughRootsOfUnity.finite_rootsOfUnity, Projectivization.generalLinearGroup_smul_def, AddAut.mulLeft_apply_symm_apply, NumberField.Units.finiteIndex_iff_sup_torsion_finiteIndex, WeierstrassCurve.Jacobian.smul_eq, Subgroup.IsArithmetic.finiteIndex_comap, IsPrimitiveRoot.val_inv_toRootsOfUnity_coe, mem_rootsOfUnity', ClassGroup.equiv_mk0, Subgroup.ofUnits_right_inverse, Matrix.SpecialLinearGroup.discreteSpecialLinearGroupIntRange, WeierstrassCurve.Jacobian.addMap_eq, NumberField.Units.instFiniteIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion, EisensteinSeries.eisensteinSeries_SIF_MDifferentiable, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, card_rootsOfUnity, MonoidWithZeroHom.inv_mem_valueGroup, Lagrange.nodal_subgroup_eq_X_pow_card_sub_one, ModularGroup.det_coe, FiniteField.sum_subgroup_units, ValuationSubring.ker_unitGroupToResidueFieldUnits, MulChar.apply_mem_rootsOfUnity_orderOf, ModularForm.coe_translate, val_rootsOfUnityEquivOfPrimitiveRoots_apply_coe, ClassGroup.equivPic_apply, IsDedekindDomain.HeightOneSpectrum.valuation_of_unit_mod_eq, ModularForm.coe_trace, WeierstrassCurve.Jacobian.negMap_eq, Matrix.GLPos.coe_neg_GL, smul_eq_mul, Subgroup.ofUnits_iSup, Unitization.val_unitsFstOne_mulEquiv_quasiregular_apply, Subgroup.instHasDetOneMapSpecialLinearGroupGeneralLinearGroupMapGL, autAdjoinRootXPowSubC_root, NumberField.Units.dirichletUnitTheorem.logEmbedding_ker, Subgroup.mem_units_iff_val_mem, NumberField.IsCMField.map_unitsMulComplexConjInv_torsion, EisensteinSeries.eisensteinSeriesSIF_mdifferentiable, HahnSeries.val_toOrderTopSubOnePos_coe, LinearEquiv.smul_refl, HahnSeries.mem_orderTopSubOnePos_iff, rootsOfUnityEquivNthRoots_symm_apply, ModularGroup.coeHom_apply, Subgroup.strictWidthInfty_SL2Z, HahnSeries.val_inv_toOrderTopSubOnePos_coe, Unitization.unitsFstOne_val_val_fst, Valuation.IsRankOneDiscrete.exists_generator_lt_one, IsPrimitiveRoot.zmodEquivZPowers_apply_coe_int, WeierstrassCurve.Jacobian.addMap_of_Y_eq, instSubsingletonSubtypeUnitsMemSubgroupRootsOfUnityOfNatNat, NumberField.IsCMField.complexConj_torsion, MulChar.apply_mem_rootsOfUnity, ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk, rootsOfUnityEquivOfPrimitiveRoots_symm_apply, Subgroup.IsArithmetic.discreteTopology, map_rootsOfUnity, ClassGroup.mk_def, ValuationSubring.coe_unitGroupToResidueFieldUnits_apply, Submonoid.units_mono, modularCyclotomicCharacter.aux_spec, WeierstrassCurve.Projective.nonsingularLift_zero, Subgroup.IsArithmetic.conj, SlashInvariantForm.coe_norm, ZMod.rootsOfUnityAddChar_val, Subgroup.ofUnits_sup_units, ValuationSubring.principalUnitGroup_injective, rootsOfUnity_zero, modularCyclotomicCharacter.toFun_spec'', NumberField.IsCMField.index_unitsMulComplexConjInv_range_dvd, instDiscreteTopologySubtypeGeneralLinearGroupMemSubgroupAdjoinNegOneOfIsTopologicalRingOfT2Space, Submodule.ker_unitsMap_spanSingleton, Unitization.mem_unitsFstOne, Submonoid.mem_units_of_val_mem_inv_val_mem, IsCusp.smul, cyclotomicCharacter.toFun_spec, SpecialLinearGroup.centerEquivRootsOfUnity_apply_of_finrank_le_one, ClassGroup.equiv_mk, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_zpow, IsDedekindDomain.selmerGroup.valuation_ker_eq, Unitization.unitsFstOne_val_inv_val_fst, ValuationSubring.principalUnitGroup_symm_apply, NumberField.Units.instFreeIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion, mem_rootsOfUnity_prime_pow_mul_iff, Submodule.unitsQuotEquivRelPic_apply_coe, IsPrimitiveRoot.map_rootsOfUnity, SlashInvariantForm.T_zpow_width_invariant, EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF, rootsOfUnity.eq_one, Matrix.GLPos.coe_neg, autEquivRootsOfUnity_smul
|
instInhabited π | CompOp | 1 mathmath: Valued.toUniformSpace_eq
|
instInv π | CompOp | 344 mathmath: CircleDeg1Lift.units_inv_apply_apply, units_inv_smul, WeierstrassCurve.j_of_char_two, spectrum.inv_mem_iff, commute_iff_inv_mul_cancel, IsLocalization.mul_add_inv_left, mul_inv_of_eq, OrderMonoidIso.val_inv_unitsWithZero_symm_apply, le_mul_inv_of_mul_le, CircleDeg1Lift.translate_inv_apply, commute_inv_coe, val_inv_unitsEquivProdSubtype_symm_apply, StandardEtalePair.inv_aeval_X_g, CFC.inv_nonneg, spectrum.of_invβ_mem, IsUnit.unit_inv_map, spectrum.invβ_mem_iff, mul_inv_le_one_of_le, IsUnit.unit_inv, val_inv_unitarySubgroupUnitsEquiv_symm_apply_coe, spectrum.units_smul_resolvent_self, AddAut.mulRight_symm_apply, inv_mul_le_of_le_mul, Matrix.trace_units_conj, mul_inv_le_one, NormedRing.inverse_add_norm_diff_nth_order, SlashInvariantForm.quotientFunc_mk, WeierstrassCurve.variableChange_aβ, Module.Basis.repr_isUnitSMul, Commute.units_inv_right_iff, Submonoid.inv_mem_units_iff, OreLocalization.universalHom_apply, WeierstrassCurve.variableChange_Ξ', pinGroup.val_inv_toUnits_apply, Matrix.GeneralLinearGroup.map_inv_mul_map, ENNReal.mulRightOrderIso_symm_apply, Matrix.charpoly_units_conj', IsUnit.mul_val_inv, inv_eq_self_iff, IsLocalizedModule.iso_apply_mk, CategoryTheory.CatCenter.smul_iso_inv_eq', Matrix.GeneralLinearGroup.isParabolic_conj_iff, MonoidHom.toHomPerm_apply_symm_apply, IsPrimitiveRoot.pow_sub_one_eq_geom_sum_mul_geom_sum_inv_mul_pow_sub_one, inv_eq_of_mul_eq_one_right, WeierstrassCurve.j_of_char_three, quasispectrum.mem_iff_of_isUnit, PreQuasiregular.add_inv_add_mul_eq_zero, Complex.conj_rootsOfUnity, one_le_inv_of_le, Polynomial.monic_of_isUnit_leadingCoeff_inv_smul, CongruenceSubgroup.exists_Gamma_le_conj, Matrix.det_units_conj', PreQuasiregular.inv_add_add_mul_eq_zero, Matrix.coe_units_inv, LocalizedModule.lift'_mk, val_inv_eq_inv_val, inv_le_one, CategoryTheory.CatCenter.smul_iso_inv_eq'_assoc, Asymptotics.isBigOWith_self_const_mul', unitsEquivProdSubtype_apply_coe, NormalizationMonoid.normUnit_coe_units, val_inv_inj, mul_liftRight_inv, PowerSeries.IsWeierstrassFactorization.isWeierstrassDivision, IsUnit.inv_smul, inv_eq_val_inv, SlashInvariantForm.coe_translate, spinGroup.val_inv_toUnits_apply, mul_inv_mem_unitary, Matrix.inv_smul', hasFDerivAt_ringInverse, mul_inv_eq_iff_eq_mul, CFC.rpow_neg, CircleDeg1Lift.coe_toOrderIso_symm, WeierstrassCurve.variableChange_bβ, Submonoid.coe_inv_val_mul_coe_val, conj_pow', PowerSeries.coeff_invOfUnit, Set.units_inv_mem_center, CircleDeg1Lift.coe_toOrderIso_inv, OrderMonoidIso.val_inv_unitsCongr_symm_apply, ZMod.dft_comp_unitMul, inv_mul, LinearMap.GeneralLinearGroup.ofLinearEquiv_inv, spinGroup.units_involute_act_eq_conjAct, MvPowerSeries.constantCoeff_invOfUnit, Module.End.algebraMap_isUnit_inv_apply_eq_iff', spectrum.resolvent_eq, Submonoid.coe_val_mul_coe_inv_val, val_inv_unitsNonZeroDivisorsEquiv_symm_apply_coe, Submonoid.inv_mem_units, fderiv_inverse, Algebra.SubmersivePresentation.jacobianRelations_spec, coe_map_inv, CircleDeg1Lift.units_apply_inv_apply, inv_mul_le_one_of_le, DihedralGroup.oddCommuteEquiv_symm_apply, mul_inv_eq_mul_inv_iff, CategoryTheory.Preadditive.smul_iso_inv, Module.Basis.det_unitsSMul, spinGroup.involute_act_ΞΉ_mem_range_ΞΉ, IsStarNormal.val_inv, Int.units_inv_eq_self, Submonoid.val_inv_unitsTypeEquivIsUnitSubmonoid_symm_apply, Polynomial.roots_C_mul_X_sub_C_of_IsUnit, WeierstrassCurve.variableChange_bβ, AffineEquiv.coe_homothetyUnitsMulHom_apply_symm, CommMonCat.val_inv_units_map_hom_apply, PowerSeries.constantCoeff_invOfUnit, Algebra.SubmersivePresentation.map_invJacobianOfHasCoeffs, WeierstrassCurve.variableChange_bβ, ZMod.inv_coe_unit, IsCyclic.val_inv_mulAutMulEquiv_apply, ContinuousLinearEquiv.symm_smul_apply, WeierstrassCurve.VariableChange.inv_def, LinearMap.GeneralLinearGroup.toLinearEquiv_inv, Submonoid.LocalizationMap.inv_unique, mul_inv_cancel_right, Matrix.GeneralLinearGroup.map_inv, inv_eq_of_mul_eq_one_left, ConjAct.units_smul_def, spectrum.units_conjugate, MulEquiv.val_inv_piUnits_apply, inv_mk, IsLocalization.lift_mk', Orientation.map_eq_det_inv_smul, mul_inv_le_iff, CStarAlgebra.inv_le_inv_iff, one_le_inv, inv_unique, Nonneg.val_inv_unitsHomeomorphPos_symm_apply_coe, IsLocalizedModule.fromLocalizedModule_mk, WithZero.val_inv_expOrderIso_apply, Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, WeierstrassCurve.variableChange_def, spectrum.invβ_mem_inv_iff, commute_iff_inv_mul_cancel_assoc, Matrix.inv_adjugate, mulLeft_symm, IsUnit.mul_liftRight_inv, Commute.units_inv_left_iff, mul_inv, inv_pos, val_inv_ofPowEqOne, ContinuousMap.unitsLift_apply_inv_apply, CStarAlgebra.inv_le_one, WeierstrassCurve.variableChange_aβ, WeierstrassCurve.variableChange_aβ, inv_mul_le_iff, CStarAlgebra.inv_le_iff, ENNReal.mulLeftOrderIso_symm_apply, CStarAlgebra.le_inv_iff, CuspForm.coe_translate, OrderMonoidIso.val_inv_unitsCongr_apply, ContinuousLinearEquiv.symm_smul, WeierstrassCurve.variableChange_cβ, Submonoid.LocalizationMap.lift_mk', inv_pow_eq_pow_inv, commute_coe_inv, NormedRing.inverse_add, Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_apply, liftRight_inv_mul, NormedRing.inverse_one_sub, mul_eq_one_iff_eq_inv, LinearEquiv.symm_smul, val_inv_cfcRpow, NormedSpace.exp_units_conj', WeierstrassCurve.coe_inv_variableChange_Ξ', WeierstrassCurve.inv_variableChange_Ξ', CFC.rpow_neg_one_eq_inv, Matrix.nonsing_inv_apply, map_units_inv, inv_mul_eq_one, mul_inv_eq_one, NormedRing.inverse_add_norm_diff_second_order, CStarAlgebra.one_le_inv_iff_le_one, LaurentPolynomial.evalβ_C_mul_T_neg_n, Matrix.charpoly_units_conj, Matrix.GeneralLinearGroup.isParabolic_conj_iff', mul_inv_cancel_left, smul_inv, one_divp, AlgEquiv.algHomUnitsEquiv_apply_symm_apply, AddConstEquiv.coe_val_inv_equivUnits_apply, continuous_iff, cfc_inv_id, Commute.units_inv_left, CategoryTheory.CatCenter.smul_iso_inv_eq_assoc, RingPreordering.unitsInv_mem, Ring.inverse_unit, WeierstrassCurve.variableChange_Ξ, ContinuousLinearEquiv.unitsEquivAut_apply_symm, WeierstrassCurve.coe_inv_map_Ξ', WeierstrassCurve.variableChange_aβ, val_inv_cfcUnits, isGroupLikeElem_unitsInv, CStarAlgebra.inv_le_inv, AffineEquiv.equivUnitsAffineMap_symm_apply_symm_apply, NumberField.IsCMField.unitsMulComplexConjInv_apply, OreLocalization.universalMulHom_apply, coe_inv_smul, Unitary.val_inv_toUnits_apply, topology_eq_inf, hasStrictFDerivAt_ringInverse, Submonoid.inv_val_mem_of_mem_units, Matrix.GeneralLinearGroup.coe_inv, spectrum.map_inv, LocalizedModule.lift_mk, eq_inv_of_mul_eq_one_right, IsUnit.val_subInvSMul, conj_pow, one_le_inv_mul_of_le, Commute.units_inv_right, Matrix.exp_units_conj', Submonoid.LocalizationMap.lift_apply, inv_mul_eq_inv_mul_iff, Algebra.SubmersivePresentation.aeval_invJacobianOfHasCoeffs, Submonoid.mem_units_iff, Matrix.GeneralLinearGroup.map_mul_map_inv, Module.Basis.det_inv, Matrix.GeneralLinearGroup.val_inv_det_apply, IsUnit.val_inv_unit', Polynomial.coeff_inv_units, eq_mul_inv_iff_mul_eq, CircleDeg1Lift.translationNumber_conj_eq, CongruenceSubgroup.mem_conjGL, inv_mul_of_eq, CategoryTheory.CatCenter.smul_iso_inv_eq, add_eq_mul_one_add_div, Module.Basis.map_orientation_eq_det_inv_smul, inv_mul_cancel_right, Polynomial.newtonMap_apply_of_isUnit, Algebra.SubmersivePresentation.exists_sum_eq_Ο_jacobian_mul_Ο_jacobian_inv_sub_one, Matrix.GeneralLinearGroup.val_inv_scalar_apply, spectrum.units_conjugate', SemiconjBy.units_inv_symm_left_iff, Asymptotics.IsBigOWith.const_mul_right', AlgEquiv.val_inv_algHomUnitsEquiv_symm_apply, continuous_coe_inv, MvPowerSeries.coeff_invOfUnit, CategoryTheory.TwistShiftData.shiftFunctorAdd'_inv_app, LaurentPolynomial.evalβ_T_neg_n, le_inv_mul_of_mul_le, mulRight_symm, CongruenceSubgroup.mem_conjGL', toAut_inv, inv_neg, PowerSeries.invOneSubPow_eq_inv_one_sub_pow, PowerSeries.IsWeierstrassDivision.isWeierstrassFactorization, divp_inv, Equiv.Perm.equivUnitsEnd_symm_apply_symm_apply, commute_iff_mul_inv_cancel_assoc, NormedRing.inverse_add_norm_diff_first_order, Submonoid.LocalizationMap.mul_inv_right, inv_eq_one_divp, GroupLike.val_inv_toUnits_apply, MonCat.val_inv_units_map_hom_apply, nnnorm_commutator_units_sub_one_le, IsUnit.val_inv_subInvSMul, WeierstrassCurve.coe_variableChange_Ξ', LinearEquiv.coe_inv_det, IsLocalizedModule.fromLocalizedModule'_mk, pinGroup.involute_act_ΞΉ_mem_range_ΞΉ, one_le_mul_inv, Module.Basis.orientation_unitsSMul, one_le_inv_mul, ArithmeticFunction.inv_zetaUnit, Submonoid.LocalizationMap.mul_inv_left, uzpow_neg, norm_commutator_units_sub_one_le, le_inv_mul_iff, IsOfFinOrder.val_inv_unit, WeierstrassCurve.inv_map_Ξ', AffineEquiv.val_inv_equivUnitsAffineMap_apply, spectrum.invβ_mem_inv, LinearMap.trace_conj, IsUnit.val_inv_apply, coe_star_inv, CircleDeg1Lift.translationNumber_conj_eq', AddConstEquiv.equivUnits_symm_apply_symm_apply, Matrix.det_units_conj, LinearEquiv.symm_smul_apply, Submonoid.unit_mem_leftInv, IsPrimitiveRoot.val_inv_toRootsOfUnity_coe, CircleDeg1Lift.translationNumber_units_inv, le_mul_inv_iff, Submonoid.LocalizationMap.mul_inv, ContinuousMap.unitsLift_symm_apply_apply_inv', IsGroupLikeElem.unitsInv, Matrix.trace_units_conj', SemiconjBy.units_inv_symm_left, spectrum.inv_mem_resolventSet, MonoidWithZeroHom.inv_mem_valueGroup, inv_le_one_of_le, inv_mul_eq_iff_eq_mul, NormedRing.inverse_add_nth_order, Matrix.GeneralLinearGroup.val_inv_swap, Submonoid.LocalizationMap.liftβ_apply, lipschitzGroup.involute_act_ΞΉ_mem_range_ΞΉ, ModularForm.coe_translate, IsUnit.val_inv_mul, Nonneg.val_inv_unitsEquivPos_symm_apply_coe, eq_inv_of_mul_eq_one_left, IsUnit.liftRight_inv_mul, Module.Basis.repr_unitsSMul, Submonoid.IsUnit.Submonoid.coe_inv, spectrum.units_smul_resolvent, mul_inv_le_of_le_mul, invOf_units, Matrix.exp_units_conj, NormedSpace.exp_units_conj, PowerSeries.IsWeierstrassDivisorAt.seq_one, SemiconjBy.units_inv_right_iff, Polynomial.roots_C_mul_X_add_C_of_IsUnit, WeierstrassCurve.variableChange_cβ, Module.Basis.coord_unitsSMul, Equiv.Perm.val_inv_equivUnitsEnd_apply, HahnSeries.val_inv_toOrderTopSubOnePos_coe, SemiconjBy.units_inv_right, commute_iff_mul_inv_cancel, Ring.inverse_of_isUnit, WeierstrassCurve.variableChange_aβ, eq_inv_mul_iff_mul_eq, PowerSeries.derivative_inv, inv_mul_le_one, CStarAlgebra.inv_le_one_iff_one_le, one_le_mul_inv_of_le, CategoryTheory.CommShiftβSetup.hΞ΅, CFC.inv_nonneg_of_nonneg, mk_semiconjBy, Module.End.algebraMap_isUnit_inv_apply_eq_iff, WithZero.val_inv_logOrderIso_symm_apply, AffineEquiv.equivUnitsAffineMap_symm_apply_invFun, mul_eq_one_iff_inv_eq, cfc_comp_inv, inv_mul_mem_unitary, Unitization.unitsFstOne_val_inv_val_fst, embedProduct_apply, val_inv_unitOfInvertible, MulEquiv.val_inv_piUnits_symm_apply, le_iff_norm_sqrt_mul_sqrt_inv, inv_mul_cancel_left, WeierstrassCurve.variableChange_bβ
|
instMonoid π | CompOp | 144 mathmath: units_inv_smul, Matrix.GeneralLinearGroup.det_scalar, ModularForm.smul_slash, mem_rootsOfUnity, SlashInvariantForm.slash_action_eq', ModularForm.mul_slash, Subgroup.HasDetPlusMinusOne.isParabolic_iff_of_upperTriangular, Matrix.GeneralLinearGroup.IsParabolic.parabolicFixedPoint_pow, UpperHalfPlane.re_smul, OnePoint.isBoundedAt_iff_exists_SL2Z, Equiv.Perm.sign_of_cycleType, ZMod.units_pow_card_sub_one_eq_one, Module.Ray.neg_units_smul, IsCusp.smul_of_mem, toMul_uzpow, UpperHalfPlane.tendsto_smul_atImInfty, SlashInvariantForm.quotientFunc_mk, smul_coe, ModularForm.SL_slash, UpperHalfPlane.im_smul_eq_div_normSq, WeierstrassCurve.variableChange_Ξ', Module.Ray.units_smul_of_neg, ModularForm.prod_slash, Complex.isQuotientCoveringMap_npow, OnePoint.smul_infty_eq_self_iff, ModularForm.prod_slash_sum_weights, SlashInvariantForm.quotientFunc_smul, ModularGroup.sl_moeb, OnePoint.isZeroAt_iff_exists_SL2Z, mem_rootsOfUnity_prime_pow_mul_iff', UpperHalfPlane.glPos_smul_def, UpperHalfPlane.J_sq, Polynomial.natDegree_of_dvd_cyclotomic_of_irreducible, isOfFinOrder_val, Fin.sign_cycleRange, UpperHalfPlane.denom_cocycle_Ο, orderOf_units, Equiv.Perm.sign_of_cycleType_eq_replicate, SlashInvariantForm.coe_translate, Matrix.GeneralLinearGroup.upperRightHom_apply, ZMod.pow_totient, pow_ofPowEqOne, isCusp_SL2Z_iff', OnePoint.smul_some_eq_ite, units_smul_eq_self_iff, units_smul_eq_neg_iff, FiniteField.forall_pow_eq_one_iff, coe_smul, Int.units_pow_two, OnePoint.map_smul, Matrix.GeneralLinearGroup.IsParabolic.pow, ArithmeticFunction.pow_carmichael, modularCyclotomicCharacter.toFun_spec, isQuotientCoveringMap_npow, UpperHalfPlane.coe_smul_of_det_pos, Submodule.linearEquiv_det_reflection, PowerSeries.coeff_invUnitsSub, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_pow', Module.Ray.units_smul_of_pos, Orientation.map_eq_det_inv_smul, Matrix.GeneralLinearGroup.isParabolic_iff_of_upperTriangular_of_det, unitary_eq, Matrix.GeneralLinearGroup.continuous_upperRightHom, UpperHalfPlane.im_smul, OnePoint.IsZeroAt.smul_iff, LinearOrderedCommGroupWithZero.inl_eq_coe_inlβ, UpperHalfPlane.coe_smul, Int.units_pow_eq_pow_mod_two, Fin.sign_cycleIcc_of_le, Equiv.Perm.sign_of_pow_two_eq_one, MDifferentiable.slash, ZMod.euler_criterion_units, Matrix.GeneralLinearGroup.fixpointPolynomial_aeval_eq_zero_iff, inv_pow_eq_pow_inv, sq_eq_sq_iff_eq_or_eq_neg, cfcUnits_pow, WeierstrassCurve.inv_variableChange_Ξ', IsPrimitiveRoot.zmodEquivZPowers_symm_apply_pow, UpperHalfPlane.J_smul, FiniteField.unit_isSquare_iff, SlashInvariantForm.slash_action_eqn'', IsCyclotomicExtension.Rat.Three.Units.mem, OnePoint.smul_infty_eq_ite, Algebra.smul_units_def, UpperHalfPlane.coe_J_smul, NumberField.Units.coe_pow, coe_inv_smul, OnePoint.IsBoundedAt.smul_iff, LinearOrderedCommGroupWithZero.inr_eq_coe_inrβ, IsPrimitiveRoot.eq_pow_of_mem_rootsOfUnity, LucasLehmer.order_Ο, ZMod.natCast_smul_units, OnePoint.smul_infty_def, Module.Basis.map_orientation_eq_det_inv_smul, Int.units_sq, cosetToCuspOrbit_apply_mk, OnePoint.exists_mem_SL2, IsPrimitiveRoot.isPrimitiveRoot_iff', PowerSeries.invOneSubPow_eq_inv_one_sub_pow, ArithmeticFunction.carmichael_eq_exponent', AlgEquiv.smul_units_def, Subgroup.mem_strictPeriods_iff, ModularForm.prod_fintype_slash, TensorProduct.CompatibleSMul.unit, ArithmeticFunction.carmichael_eq_exponent, NumberField.Units.instFGUnitsRingOfIntegers, ModularForm.slash_def, Polynomial.natDegree_of_mem_normalizedFactors_cyclotomic, UpperHalfPlane.instContinuousGLSMul, Module.Basis.orientation_unitsSMul, Matrix.det_neg_eq_smul, ModularForm.is_invariant_one', Polynomial.orderOf_root_cyclotomic_dvd, sign_finRotate, Equiv.Perm.IsCycle.sign, SlashInvariantFormClass.norm_petersson_smul, IsUnit.unit_pow, val_pow_eq_pow_val, IsPrimitiveRoot.zmodEquivZPowers_apply_coe_nat, Projectivization.generalLinearGroup_smul_def, SlashInvariantForm.slash_action_eqn', UpperHalfPlane.IsZeroAtImInfty.slash, Equiv.Perm.sign_prod_list_swap, ModularForm.coe_translate, UpperHalfPlane.neg_smul, SlashInvariantFormClass.petersson_smul, Equiv.Perm.sign_of_cycleType', smul_eq_mul, UpperHalfPlane.contMDiff_smul, Matrix.GeneralLinearGroup.injective_upperRightHom, ZMod.orderOf_units_dvd_card_sub_one, Matrix.GeneralLinearGroup.IsParabolic.smul_eq_self_iff, SlashInvariantFormClass.slash_action_eq, CircleDeg1Lift.translate_pow, SlashInvariantForm.slash_action_eqn, ZMod.smul_units_def, Polynomial.normalizedFactors_cyclotomic_card, UpperHalfPlane.IsBoundedAtImInfty.slash, IsCusp.smul, UpperHalfPlane.mdifferentiable_smul, QuadraticForm.equivalent_weightedSumSquares_units_of_nondegenerate', ModularForm.slash_apply, ofMul_uzpow, UpperHalfPlane.petersson_slash
|
instMul π | CompOp | 205 mathmath: Set.center_units_subset, IsUnit.unit_mul, MulChar.equivToUnitHom_mul_apply, ContinuousLinearEquiv.unitsEquiv_apply, OrderMonoidIso.val_inv_unitsWithZero_symm_apply, ValuationSubring.coe_mem_principalUnitGroup_iff, Matrix.UnitaryGroup.toGL_mul, LinearMap.GeneralLinearGroup.congrLinearEquiv_refl, NumberField.IsCMField.unitsComplexConj_torsion, WithZero.withZeroUnitsEquiv_symm_apply_coe, LinearEquiv.det_trans, WithZero.coe_unitsWithZeroEquiv_eq_units_val, IsCyclic.val_mulAutMulEquiv_apply, unitsNonZeroDivisorsEquiv_apply, OrderMonoidIso.val_unitsCongr_symm_apply, WeierstrassCurve.variableChange_Ξ', Matrix.GeneralLinearGroup.map_inv_mul_map, ComplexShape.associative_Ξ΅β_Ξ΅β, LinearOrderedCommGroupWithZero.inl_mul_inr_eq_coe_toLex, HomologicalComplex.mapBifunctorββ.dβ_eq, Set.unitEquivUnitsInteger_symm_apply_coe, Equiv.Perm.val_equivUnitsEnd_apply, Matrix.GeneralLinearGroup.coe_toLin, ComplexShape.Ξ΅_add, Matrix.GeneralLinearGroup.isParabolic_conj_iff, HomologicalComplex.mapBifunctorββ.dβ_eq, LinearMap.GeneralLinearGroup.generalLinearEquiv_to_linearMap, MulEquiv.val_piUnits_symm_apply, val_unitsCentralizerEquiv_apply_coe, NumberField.Units.coe_mul, CongruenceSubgroup.exists_Gamma_le_conj, RootPairing.Equiv.toEndUnit_inv, UpperHalfPlane.denom_cocycle_Ο, instStarModule, ComplexShape.Ξ΅β_Ξ΅β, ZMod.AddAutEquivUnits_symm_apply, MulChar.mulEquiv_units, mul_inv_mem_unitary, OrderMonoidIso.val_unitsCongr_apply, TotalComplexShapeSymmetry.Ο_Ξ΅β, ModularGroup.lcRow0Extend_symm_apply, Equiv.Perm.decomposeFin.symm_sign, CategoryTheory.Aut.toEnd_apply, AffineEquiv.linear_equivUnitsAffineMap_symm_apply, Commute.units_of_val, val_toUnits_apply, UpperHalfPlane.Ο_mul, CategoryTheory.TwistShiftData.assoc, OrderMonoidIso.val_inv_unitsCongr_symm_apply, OrderMonoidIso.withZeroUnits_symm_apply, WeierstrassCurve.VariableChange.mul_def, DirichletCharacter.mulEquiv_units, OrderMonoidIso.withZeroUnits_apply, val_inv_unitsNonZeroDivisorsEquiv_symm_apply_coe, OrderMonoidIso.val_unitsWithZero_symm_apply, coe_star, ComplexShape.Associative.Ξ΅β_Ξ΅β, divp_add_divp, instContinuousMul, Submonoid.val_inv_unitsTypeEquivIsUnitSubmonoid_symm_apply, Nonneg.val_unitsEquivPos_symm_apply_coe, Equiv.Perm.sign_trans, Int.negOnePow_add, IsCyclic.val_inv_mulAutMulEquiv_apply, Equiv.Perm.sign_sumCongr, UpperHalfPlane.denom_cocycle, WithZero.withZeroUnitsEquiv_symm_strictMono, ModularGroup.lcRow0Extend_apply, ComplexShape.associative_Ξ΅β_eq_mul, WithZero.unitsWithZeroEquiv_symm_apply, ValuationSubring.coe_unitGroupMulEquiv_apply, AffineEquiv.val_equivUnitsAffineMap_apply, MulEquiv.val_inv_piUnits_apply, Matrix.GeneralLinearGroup.toLin'_apply, Submonoid.unitsTypeEquivIsUnitSubmonoid_apply_coe, mapEquiv_symm, Unitization.val_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, OrderMonoidIso.unitsWithZero_apply, Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, ComplexShape.Ξ΅β_Ξ΅β, val_unitsNonZeroDivisorsEquiv_symm_apply_coe, ZMod.AddAutEquivUnits_apply, Subgroup.val_centerUnitsEquivUnitsCenter_symm_apply_coe, symm_mapContinuousMulEquiv, Int.units_div_eq_mul, OrderMonoidIso.val_inv_unitsCongr_apply, MonoidWithZeroHom.inl_mul_inr_eq_mk_of_unit, Set.val_unitEquivUnitsInteger_apply_coe, IsCyclotomicExtension.Rat.galEquivZMod_apply_of_pow_eq, Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_apply, coe_unop_opEquiv, ComplexShape.Ο_Ξ΅β, Subgroup.mem_ofUnits_iff_toUnits_mem, LinearMap.GeneralLinearGroup.congrLinearEquiv_apply, toAut_hom, ComplexShape.associative_Ξ΅β_eq_mul, AffineEquiv.equivUnitsAffineMap_symm_apply_apply, Equiv.Perm.sign_mul, WeierstrassCurve.inv_variableChange_Ξ', Nonneg.unitsEquivPos_apply_coe, mk0_mul, FiniteField.unit_isSquare_iff, Equiv.Perm.signAux3_mul_and_swap, IsCyclotomicExtension.Rat.galEquivZMod_restrictNormal_apply, val_unitsCentralizerEquiv_symm_apply_coe, Matrix.GeneralLinearGroup.isParabolic_conj_iff', Subgroup.val_centerUnitsEquivUnitsCenter_apply_coe, WithZero.toMonoidWithZeroHom_withZeroUnitsEquiv, AlgEquiv.algHomUnitsEquiv_apply_symm_apply, AddConstEquiv.coe_val_inv_equivUnits_apply, AlgEquiv.val_algHomUnitsEquiv_symm_apply, instContinuousStarUnits, TotalComplexShapeSymmetry.Ο_Ξ΅β, uzpow_add, divp_divp_eq_divp_mul, ComplexShape.Ο_Ξ΅β, AffineEquiv.equivUnitsAffineMap_symm_apply_symm_apply, NumberField.IsCMField.unitsMulComplexConjInv_apply, ClassGroup.mk_eq_mk, AddConstEquiv.equivUnits_symm_apply_apply, PowerSeries.invOneSubPow_add, Int.negOnePow_sub, AffineEquiv.equivUnitsAffineMap_symm_apply_toFun, NumberField.IsCMField.unitsComplexConj_eq_self_iff, Matrix.GeneralLinearGroup.map_mul_map_inv, toMulEquiv_mapContinuousMulEquiv, CongruenceSubgroup.mem_conjGL, Commute.units_val_iff, LinearMap.GeneralLinearGroup.congrLinearEquiv_symm, ValuationSubring.coe_unitGroupMulEquiv_symm_apply, ComplexShape.Associative.Ξ΅β_eq_mul, AlgEquiv.val_inv_algHomUnitsEquiv_symm_apply, SemiconjBy.units_of_val, ComplexShape.Associative.Ξ΅β_eq_mul, IsCyclic.mulAutMulEquiv_symm_apply_symm_apply, CongruenceSubgroup.mem_conjGL', toAut_inv, NormalizationMonoid.normUnit_mul, nonZeroDivisorsEquivUnits_apply, Equiv.Perm.equivUnitsEnd_symm_apply_symm_apply, toUnits_symm_apply, coe_opEquiv_symm, Set.subset_center_units, nnnorm_commutator_units_sub_one_le, nonZeroDivisorsEquivUnits_symm_apply_coe, Set.center_units_eq, WithZero.withZeroUnitsEquiv_symm_apply, LinearMap.GeneralLinearGroup.congrLinearEquiv_trans', LinearMap.GeneralLinearGroup.toLinearEquiv_mul, Equiv.Perm.equivUnitsEnd_symm_apply_apply, toUnits_val_apply, embed_product_star, UpperHalfPlane.mul_smul', IsCyclic.mulAutMulEquiv_symm_apply_apply, norm_commutator_units_sub_one_le, Subgroup.mem_iff_toUnits_mem_units, NumberField.Units.exist_unique_eq_mul_prod, Matrix.GeneralLinearGroup.map_mul, AffineEquiv.val_inv_equivUnitsAffineMap_apply, coe_star_inv, SemiconjBy.units_val_iff, Matrix.GeneralLinearGroup.coe_mul, AddConstEquiv.equivUnits_symm_apply_symm_apply, LinearMap.GeneralLinearGroup.congrLinearEquiv_trans, LinearMap.GeneralLinearGroup.ofLinearEquiv_mul, divp_sub_divp, divp_mul_divp, WithZero.withZeroUnitsEquiv_apply, UpperHalfPlane.denom_cocycle', mul_uzpow, Nonneg.val_inv_unitsEquivPos_symm_apply_coe, HomologicalComplex.mapBifunctorββ.dβ_eq, Submonoid.val_unitsTypeEquivIsUnitSubmonoid_symm_apply, MulEquiv.val_piUnits_apply, smul_eq_mul, Equiv.Perm.sign_subtypeCongr, Unitization.val_unitsFstOne_mulEquiv_quasiregular_apply, HomologicalComplex.mapBifunctorββ.dβ_eq, Equiv.Perm.val_inv_equivUnitsEnd_apply, MonoidWithZeroHom.commute_inl_inr, TotalComplexShape.Ξ΅β_Ξ΅β, LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv, ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk, AddConstEquiv.coe_val_equivUnits_apply, mapContinuousMulEquiv_apply, val_mul, ValuationSubring.coe_unitGroupToResidueFieldUnits_apply, CategoryTheory.CommShiftβSetup.hΞ΅, coe_mapEquiv, AffineEquiv.equivUnitsAffineMap_symm_apply_invFun, IsCyclotomicExtension.autEquivPow_symm_apply, WithZero.unitsWithZeroEquiv_apply, AlgEquiv.algHomUnitsEquiv_apply_apply, ClassGroup.equiv_mk, Matrix.GeneralLinearGroup.toLin_apply, Submonoid.mul_mem_units, inv_mul_mem_unitary, WithZero.withZeroUnitsEquiv_strictMono, RootPairing.Equiv.toEndUnit_val, IsCyclotomicExtension.autEquivPow_apply, Equiv.Perm.signAux_mul, MulEquiv.val_inv_piUnits_symm_apply, IsCyclotomicExtension.Rat.galEquivZMod_smul_of_pow_eq, Int.units_mul_self, Equiv.Perm.OnCycleFactors.sign_kerParam_apply_apply
|
instMulOneClass π | CompOp | 435 mathmath: Fin.sign_cycleIcc_of_eq, IsLocalization.mul_add_inv_left, Matrix.GeneralLinearGroup.det_scalar, MulChar.equivToUnitHom_mul_apply, AlternatingMap.domCoprod.summand_mk'', Matrix.det_apply, ValuationSubring.coe_mem_principalUnitGroup_iff, Matrix.SpecialLinearGroup.map_mapGL, Complex.linearEquiv_det_conjLIE, CircleDeg1Lift.translate_inv_apply, ClassGroup.mk0_integralRep, ZMod.unitsMap_surjective, Matrix.GeneralLinearGroup.map_det, NumberField.Units.logEmbedding_fundSystem, Matrix.SpecialLinearGroup.continuous_toGL, MulChar.toUnitHom_eq, ModularForm.mul_slash, MonoidWithZeroHom.snd_comp_inl, ClassGroup.mk_eq_mk_of_coe_ideal, Matrix.SpecialLinearGroup.coeToGL_det, Matrix.GeneralLinearGroup.map_comp_apply, Orientation.linearEquiv_det_rotation, LinearEquiv.transvection.det_eq_one, ContinuousMultilinearMap.alternatization_apply_apply, AffineEquiv.coe_homothetyUnitsMulHom_eq_homothetyHom_coe, LinearEquiv.det_trans, OnePoint.isBoundedAt_iff_exists_SL2Z, ClassGroup.Quot_mk_eq_mk, AlternatingMap.map_perm, ZLattice.covolume_eq_det_inv, Unitary.toUnits_injective, Equiv.Perm.sign_of_cycleType, Matrix.det_permute, Representation.asGroupHom_apply, SpecialLinearGroup.coe_zpow, toMul_uzpow, CongruenceSubgroup.exists_Gamma_le_conj', SpecialLinearGroup.toLinearEquiv_symm_to_linearMap, unitsNonZeroDivisorsEquiv_apply, DirichletCharacter.changeLevel_def, ModularForm.SL_slash, CongruenceSubgroup.conjGL_coe, SpecialLinearGroup.mem_center_iff_spec, CommGroup.monoidHom_mulEquiv_of_hasEnoughRootsOfUnity, cyclotomicCharacter.toZModPow, UpperHalfPlane.im_smul_eq_div_normSq, pinGroup.val_inv_toUnits_apply, Matrix.GeneralLinearGroup.map_inv_mul_map, LinearOrderedCommGroupWithZero.inl_mul_inr_eq_coe_toLex, SpecialLinearGroup.mem_center_iff, ZMod.unitsMap_self, Valuation.instNontrivialSubtypeUnitsMemSubmonoidValueMonoidOfIsNontrivial, ker_zpowGroupHom_eq_rootsOfUnity, Ideal.torsionMapQuot_apply, UpperHalfPlane.moebius_im, ModularForm.prod_slash, Complex.isQuotientCoveringMap_npow, Equiv.Perm.sign_subtypePerm, coe_liftRight, SpecialLinearGroup.coe_one, MonoidWithZeroHom.coe_one, ModularForm.prod_slash_sum_weights, MonoidHom.toHomPerm_apply_symm_apply, Equiv.Perm.sign_trans_trans_symm, ModularGroup.sl_moeb, SpecialLinearGroup.mem_range_toGeneralLinearGroup_iff, MonoidWithZeroHom.fst_mono, Equiv.Perm.viaFintypeEmbedding_sign, OnePoint.isZeroAt_iff_exists_SL2Z, Equiv.Perm.sign_symm, MonoidHom.ker_toHomUnits, Ideal.rootsOfUnityMapQuot_injective, CongruenceSubgroup.exists_Gamma_le_conj, LinearEquiv.det_baseChange, modularCyclotomicCharacter.spec, Fin.sign_cycleRange, Equiv.Perm.sign_eq_prod_prod_Ioi, Equiv.Perm.prod_Ioi_comp_eq_sign_mul_prod, Matrix.SpecialLinearGroup.isClosedEmbedding_toGL, Valuation.unit_map_eq, alternatingGroup.normalClosure_swap_mul_swap_five, ZMod.AddAutEquivUnits_symm_apply, val_unitsCenterToCenterUnits_apply_coe, mul_liftRight_inv, CommGroup.card_monoidHom_of_hasEnoughRootsOfUnity, Equiv.Perm.sign_of_cycleType_eq_replicate, coe_map, map_mk, pinGroup.val_toUnits_apply, ComplexShape.TensorSigns.Ξ΅'_succ, spinGroup.val_inv_toUnits_apply, MonoidWithZeroHom.mem_valueMonoid, isCusp_SL2Z_iff', Equiv.Perm.decomposeFin.symm_sign, IsPrimitiveRoot.autToPow_eq_modularCyclotomicCharacter, ModularGroup.denom_apply, map_bijective, AffineEquiv.linear_equivUnitsAffineMap_symm_apply, CircleDeg1Lift.coe_toOrderIso_symm, CircleDeg1Lift.translate_iterate, Matrix.GeneralLinearGroup.continuous_det, IsPrimitiveRoot.coe_autToPow_apply, NumberField.Units.logEmbeddingQuot_apply, NumberField.Units.basisOfIsMaxRank_apply, AlternatingMap.map_congr_perm, map_neg, map_injective, unitary.toUnits_comp_map, CircleDeg1Lift.coe_toOrderIso_inv, unitSphereToUnits_apply_coe, Equiv.Perm.sign_prodExtendRight, coe_toPrincipalIdeal, MonoidWithZeroHom.inl_strictMono, instFiniteMonoidHomUnits, SpecialLinearGroup.coe_inv, Equiv.Perm.sign_abs, WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_neg_mul, Fin.sign_cycleIcc_of_ge, MulChar.equivToUnitHom_symm_coe, coe_map_inv, CommMonCat.val_units_map_hom_apply, MultilinearMap.domCoprod_alternization_coe, unitSphereToUnits_injective, Matrix.SpecialLinearGroup.mapGL_injective, OnePoint.map_smul, NumberField.Units.complexEmbedding_injective, SpecialLinearGroup.congr_linearEquiv_coe_apply, Matrix.SpecialLinearGroup.mapGL_inj, IsPrimitiveRoot.autToPow_injective, Equiv.Perm.sign_trans, AffineEquiv.coe_homothetyUnitsMulHom_apply_symm, DirichletCharacter.Even.toUnitHom_eval_neg_one, CommMonCat.val_inv_units_map_hom_apply, SpecialLinearGroup.det_eq_one, CongruenceSubgroup.IsArithmetic.conj, isQuotientCoveringMap_npow, DirichletCharacter.toUnitHom_eq_char', Equiv.Perm.sign_sumCongr, DirichletCharacter.changeLevel_toUnitHom, Equiv.Perm.sign_eq_prod_prod_Iio, ZMod.unitsMap_comp, FractionalIdeal.canonicalEquiv_mk0, Matrix.det_permutation, Matrix.GeneralLinearGroup.map_comp, NumberField.InfinitePlace.ComplexEmbedding.conjugate_sign, Submodule.linearEquiv_det_reflection, Matrix.SpecialLinearGroup.isClosedEmbedding_mapGLInt, Submonoid.LocalizationMap.inv_unique, Matrix.GeneralLinearGroup.map_inv, MonoidHom.coe_toHomUnits, Subgroup.HasDetOne.det_eq, NumberField.Units.dirichletUnitTheorem.sum_logEmbedding_component, IsLocalization.lift_mk', IsUnit.coe_liftRight, Submonoid.mk_mul_mk_inv_eq_one, CongruenceSubgroup.isArithmetic_conj_SL2Z, Submonoid.mk_inv_mul_mk_eq_one, Orientation.map_eq_det_inv_smul, MonoidWithZeroHom.fst_comp_inl, unitary.toUnits_injective, ModularGroup.denom_S, NumberField.IsCMField.unitsMulComplexConjInv_apply_torsion, LinearEquiv.det_symm, Matrix.SpecialLinearGroup.isInducing_mapGL, IsCyclic.monoidHom_equiv_self, unitary_eq, SpecialLinearGroup.centerEquivRootsOfUnity_symm_apply, Equiv.Perm.sign_bij, LinearOrderedCommGroupWithZero.inl_eq_coe_inlβ, Fin.sign_cycleIcc_of_le, SpecialLinearGroup.det_coe, MonoidHom.toHomUnits_mul, Subgroup.val_centerUnitsEquivUnitsCenter_symm_apply_coe, IsUnit.mul_liftRight_inv, Equiv.Perm.mem_alternatingGroup, Matrix.det_reindex, Equiv.Perm.sign_of_pow_two_eq_one, rootsOfUnity_eq_ker, unitsCenterToCenterUnits_injective, NumberField.mixedEmbedding.logMap_eq_logEmbedding, CuspForm.coe_translate, Equiv.Perm.sign_refl, isEmbedding_embedProduct, MonoidWithZeroHom.inl_mul_inr_eq_mk_of_unit, isOpenMap_map, Submonoid.LocalizationMap.lift_mk', unitary.val_toUnits_apply, IsDedekindDomain.HeightOneSpectrum.valuation_of_unit_eq, liftRight_inv_mul, SpecialLinearGroup.coe_mul, CircleDeg1Lift.translate_apply, Matrix.SpecialLinearGroup.toGL_injective, Submodule.unitsToPic_apply, map_id, LinearIsometryEquiv.toLinearEquiv_smul, Unitary.toAlgEquiv_conjStarAlgAut, Equiv.Perm.sign_mul, LinearEquiv.det_conj, SpecialLinearGroup.coe_pow, Matrix.SpecialLinearGroup.toLin_equiv.symm_toLinearMap_eq, MonoidWithZeroHom.inr_mono, modularCyclotomicCharacter.unique, NumberField.Units.dirichletUnitTheorem.logEmbedding_eq_zero_iff, IsCyclotomicExtension.Rat.galEquivZMod_restrictNormal_apply, Equiv.Perm.sign_symm_trans_trans, CongruenceSubgroup.finiteIndex_conjGL, Equiv.Perm.mem_ofSign, MulChar.ofUnitHom_eq, Matrix.SpecialLinearGroup.range_toGL, Matrix.SpecialLinearGroup.isEmbedding_toGL, MonoidWithZeroHom.snd_inr, MonoidWithZeroHom.snd_inl_apply_of_ne_zero, WithZero.toMonoidWithZeroHom_withZeroUnitsEquiv, isQuotientCoveringMap_zpow, CircleDeg1Lift.coe_toOrderIso, CircleDeg1Lift.translate_zpow, MonoidWithZeroHom.inl_injective, ClassGroup.mk_mk0, Unitary.toRingEquiv_conjStarAlgAut, Unitary.val_toUnits_apply, Complex.linearEquiv_det_conjAe, ModularForm.SL_slash_def, NumberField.Units.complexEmbedding_apply, ClassGroup.mk_eq_one_iff, MultilinearMap.alternatization_apply, pinGroup.toUnits_injective, toPrincipalIdeal_eq_iff, PowerSeries.map_invUnitsSub, Algebra.smul_units_def, SpecialLinearGroup.centerEquivRootsOfUnity_apply, Equiv.Perm.decomposeOption_symm_sign, WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal', Matrix.GeneralLinearGroup.map_swap, NumberField.IsCMField.unitsMulComplexConjInv_apply, GroupLike.val_toUnits_apply, ClassGroup.mk_eq_mk, Unitary.val_inv_toUnits_apply, LinearOrderedCommGroupWithZero.inr_eq_coe_inrβ, pinGroup.mem_lipschitzGroup, NumberField.mixedEmbedding.logMap_unit_smul, Equiv.Perm.sign_permCongr, Unitary.toUnits_comp_map, Continuous.units_map, LinearOrderedCommGroupWithZero.fst_comp_inl, IsLocalRing.surjective_units_map_of_local_ringHom, SlashInvariantForm.slash_action_eqn_SL'', ContinuousMultilinearMap.alternatization_apply_toContinuousMultilinearMap, ZMod.unitsMap_val, Submonoid.LocalizationMap.lift_apply, ValuationSubring.surjective_unitGroupToResidueFieldUnits, MonoidWithZeroHom.snd_mono, WeierstrassCurve.Affine.Point.toClass_some, ValuationSubring.principalUnitGroupEquiv_apply, MonCat.val_units_map_hom_apply, Subgroup.HasDetPlusMinusOne.det_eq, Matrix.GeneralLinearGroup.map_mul_map_inv, linearEquiv_det_rotation, Matrix.GeneralLinearGroup.val_inv_det_apply, SpecialLinearGroup.toGeneralLinearGroup_injective, ModularGroup.im_smul_eq_div_normSq, Matrix.SpecialLinearGroup.coe_GL_coe_matrix, MonoidWithZeroHom.fst_apply_coe, Ideal.rootsOfUnityMapQuot_apply, MonoidWithZeroHom.fst_inl, MonoidWithZeroHom.fst_surjective, MonoidWithZeroHom.valueGroup_def, CongruenceSubgroup.mem_conjGL, Matrix.SpecialLinearGroup.coe_to_GLPos_to_GL_det, Module.Basis.map_orientation_eq_det_inv_smul, map_comp, IsDedekindDomain.HeightOneSpectrum.valuationOfNeZero_eq, Matrix.det_mul_aux, MonoidWithZeroHom.snd_comp_inr, NumberField.Units.dirichletUnitTheorem.logEmbedding_component, cosetToCuspOrbit_apply_mk, MonoidWithZeroHom.valueMonoid_eq_closure, Matrix.GeneralLinearGroup.val_inv_scalar_apply, ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply, OnePoint.exists_mem_SL2, AffineEquiv.coe_homothetyUnitsMulHom_apply, Matrix.det_permute', cyclotomicCharacter.toZModPow_toFun, MonoidWithZeroHom.inr_apply_unit, MonoidWithZeroHom.valueMonoid_eq_valueGroup', Matrix.mem_glpos, Ideal.torsionMapQuot_injective, pinGroup.mem_iff, LinearOrderedCommGroupWithZero.fst_apply, isClosedEmbedding_embedProduct, Matrix.GeneralLinearGroup.val_map_apply, Polynomial.det_taylorLinearEquiv, UpperHalfPlane.det_J, MultilinearMap.alternatization_coe, CongruenceSubgroup.mem_conjGL', FiniteField.unitsMap_norm_surjective, AddAut.mulLeft_apply_apply, coeHom_apply, AlgEquiv.smul_units_def, lipschitzGroup.coe_mem_iff_mem, Submonoid.LocalizationMap.mul_inv_right, ModularGroup.exists_one_half_le_im_smul_and_norm_denom_le, MonoidWithZeroHom.fst_inr_apply_of_ne_zero, cyclotomicCharacter.spec, GroupLike.val_inv_toUnits_apply, MonCat.val_inv_units_map_hom_apply, Matrix.SpecialLinearGroup.toLin_equiv.toLinearMap_eq, continuous_embedProduct, SpecialLinearGroup.toGeneralLinearGroup_toLinearEquiv_apply, ModularForm.prod_fintype_slash, continuous_map, Matrix.GeneralLinearGroup.map_apply, Equiv.Perm.sign_extendDomain, WeierstrassCurve.map_Ξ', MonoidWithZeroHom.inr_strictMono, LinearEquiv.coe_inv_det, ModularForm.slash_def, NumberField.IsCMField.indexRealUnits_eq_two_iff, FractionalIdeal.map_canonicalEquiv_mk0, ModularForm.is_invariant_one', sign_finRotate, embed_product_star, Equiv.Perm.IsCycle.sign, IsPrimitiveRoot.autToPow_spec, Equiv.Perm.sign_inv, Submonoid.LocalizationMap.mul_inv_left, MulChar.coe_toUnitHom, ClassGroup.mk_eq_one_of_coe_ideal, DirichletCharacter.factorsThrough_iff_ker_unitsMap, Equiv.Perm.IsThreeCycle.sign, NumberField.Units.logEmbeddingEquiv_apply, toPrincipalIdeal_def, SpecialLinearGroup.coe_toGeneralLinearGroup_apply, AlternatingMap.domDomCongr_perm, Matrix.GeneralLinearGroup.map_one, Equiv.Perm.IsSwap.sign_eq, Submodule.mulExact_unitsMap_spanSingleton_unitsToPic, Matrix.GeneralLinearGroup.map_mul, modularCyclotomicCharacter'.spec', WeierstrassCurve.inv_map_Ξ', MonoidWithZeroHom.one_mem_valueMonoid, Matrix.SpecialLinearGroup.mapGL_coe_matrix, Equiv.Perm.sign_prodCongrRight, MonoidWithZeroHom.inl_mono, CircleDeg1Lift.translationNumber_translate, AddAut.mulLeft_apply_symm_apply, Equiv.Perm.sign_eq_sign_of_equiv, Equiv.Perm.sign_one, MulChar.ofUnitHom_coe, Matrix.SpecialLinearGroup.det_mapGL, Subgroup.HasDetPlusMinusOne.abs_det, ClassGroup.equiv_mk0, ModularForm.SL_slash_apply, MonoidWithZeroHom.mem_valueMonoid_iff, Submonoid.LocalizationMap.mul_inv, EisensteinSeries.eisSummand_SL2_apply, DirichletCharacter.Odd.toUnitHom_eval_neg_one, Matrix.det_apply', Equiv.Perm.sign_prod_list_swap, ValuationSubring.ker_unitGroupToResidueFieldUnits, Submonoid.LocalizationMap.liftβ_apply, Circle.toUnits_apply, ClassGroup.mk_canonicalEquiv, Matrix.GeneralLinearGroup.val_scalar_apply, Equiv.Perm.sign_prodCongrLeft, MonoidWithZeroHom.snd_apply_coe, IsUnit.liftRight_inv_mul, Matrix.GeneralLinearGroup.map_id, IsDedekindDomain.HeightOneSpectrum.valuation_of_unit_mod_eq, MonoidHom.toHomUnitsMulEquiv_symm_apply, MulChar.coe_equivToUnitHom, LinearEquiv.det_refl, Equiv.Perm.sign_of_cycleType', NumberField.Units.regulator_eq_det', Equiv.Perm.sign_subtypeCongr, LinearOrderedCommGroupWithZero.inl_apply, SpecialLinearGroup.baseChange_apply_coe, CongruenceSubgroup.IsCongruenceSubgroup.conjGL, LinearOrderedCommGroupWithZero.inr_apply, exteriorPower.toTensorPower_apply_ΞΉMulti, Equiv.Perm.prod_Iio_comp_eq_sign_mul_prod, alternatingGroup_eq_sign_ker, Equiv.optionCongr_sign, SpecialLinearGroup.coe_div, NumberField.Units.complexEmbedding_inj, range_embedProduct, MonoidWithZeroHom.inr_injective, CircleDeg1Lift.translate_pow, MonoidWithZeroHom.commute_inl_inr, MonoidWithZeroHom.fst_comp_inr, Matrix.SpecialLinearGroup.isInducing_toGL, embedProduct_injective, NumberField.Units.regOfFamily_eq_det', LinearIsometryEquiv.toContinuousLinearEquiv_smul, Submodule.mulExact_unitsToPic_mapAlgebra, MulChar.apply_mem_rootsOfUnity, ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk, isInducing_embedProduct, coeHom_injective, mapContinuousMulEquiv_apply, UpperHalfPlane.smulAux'_im, FractionalIdeal.coe_mk0, ClassGroup.mk_def, Equiv.Perm.sign_swap', SpecialLinearGroup.coe_dualMap, ValuationSubring.coe_unitGroupToResidueFieldUnits_apply, modularCyclotomicCharacter'.unique', WeierstrassCurve.Affine.Point.toClass_apply, Equiv.Perm.sign_swap, Subgroup.IsArithmetic.conj, WeierstrassCurve.VariableChange.map_u, cyclotomicCharacter.continuous, Equiv.Perm.sign_ofSubtype, spinGroup.toUnits_injective, Submodule.ker_unitsMap_spanSingleton, SpecialLinearGroup.toLinearEquiv_to_linearMap, map_neg_one, Matrix.SpecialLinearGroup.toGL_inj, ClassGroup.equiv_mk, MonoidWithZeroHom.inl_apply_unit, MonoidWithZeroHom.snd_surjective, MultilinearMap.alternatization_def, ValuationSubring.principalUnitGroup_symm_apply, Subgroup.hasDetPlusMinusOne_iff_abs_det, Matrix.SpecialLinearGroup.isEmbedding_mapGL, embedProduct_apply, LinearEquiv.coe_det, IsCyclotomicExtension.autEquivPow_apply, MonoidHom.toHomUnitsMulEquiv_apply, spinGroup.val_toUnits_apply, Equiv.Perm.sign_surjective, ModularForm.slash_apply, Equiv.Perm.OnCycleFactors.sign_kerParam_apply_apply, ofMul_uzpow, Matrix.GeneralLinearGroup.val_det_apply, UpperHalfPlane.petersson_slash
|
instOne π | CompOp | 186 mathmath: Fin.sign_cycleIcc_of_eq, Valuation.IsRankOneDiscrete.generator_lt_one, mem_rootsOfUnity, Subgroup.adjoinNegOne_eq_self_iff, Complex.linearEquiv_det_conjLIE, HNNExtension.toSubgroup_neg_one, PowerSeries.invOneSubPow_zero, Matrix.SpecialLinearGroup.coeToGL_det, normUnit_eq_one, CategoryTheory.TwistShiftData.z_zero_zero, Orientation.linearEquiv_det_rotation, NumberField.hermiteTheorem.minkowskiBound_lt_boundOfDiscBdd, LinearEquiv.transvection.det_eq_one, Equiv.Perm.sign_of_cycleType, ZMod.units_pow_card_sub_one_eq_one, Valuation.IsRankOneDiscrete.exists_generator_lt_one', PUnit.norm_unit_eq, ComplexShape.eulerCharSignsDownNat_Ο, SpecialLinearGroup.coe_zpow, SpecialLinearGroup.toLinearEquiv_symm_to_linearMap, SpecialLinearGroup.mem_center_iff_spec, uzpow_zero, PowerSeries.Unit_of_divided_by_X_pow_order_zero, Matrix.detp_neg_one_one, Matrix.GeneralLinearGroup.map_inv_mul_map, Equiv.Perm.signAux_swap, SpecialLinearGroup.mem_center_iff, inv_eq_self_iff, HNNExtension.NormalWord.t_smul_eq_unitsSMul, SpecialLinearGroup.coe_one, normUnit_mul_normUnit, MonoidWithZeroHom.coe_one, Int.negOnePow_eq_neg_one_iff, SpecialLinearGroup.mem_range_toGeneralLinearGroup_iff, coe_neg_one, mem_rootsOfUnity_prime_pow_mul_iff', Int.normUnit_eq, UpperHalfPlane.J_sq, Fin.sign_cycleRange, Equiv.Perm.sign_eq_prod_prod_Ioi, Polynomial.normUnit_content, alternatingGroup.normalClosure_swap_mul_swap_five, HNNExtension.toSubgroupEquiv_neg_one, Equiv.Perm.sign_of_cycleType_eq_replicate, PowerSeries.normUnit_X, GradedTensorProduct.tmul_coe_mul_coe_tmul, ZMod.pow_totient, ComplexShape.Ξ΅_down_β, pow_ofPowEqOne, WeierstrassCurve.toCharNeTwoNF_u, Equiv.Perm.decomposeFin.symm_sign, HNNExtension.toSubgroup_one, CliffordAlgebra.map_mul_map_of_isOrtho_of_mem_evenOdd, Int.negOnePow_two_mul, NormalizationMonoid.normUnit_zero, SpecialLinearGroup.coe_inv, FiniteField.forall_pow_eq_one_iff, Fin.sign_cycleIcc_of_ge, Nat.units_eq_one, Matrix.detp_one_one, ComplexShape.Ξ΅β_def, Int.units_pow_two, Subgroup.negOne_mem_adjoinNegOne, Matrix.det_eq_detp_sub_detp, SpecialLinearGroup.congr_linearEquiv_coe_apply, DirichletCharacter.Even.toUnitHom_eval_neg_one, ArithmeticFunction.pow_carmichael, Equiv.Perm.signAux_one, SpecialLinearGroup.det_eq_one, WeierstrassCurve.Affine.nonsingular_iff_variableChange, UnitsInt.univ, WeierstrassCurve.Affine.equation_iff_variableChange, Equiv.Perm.sign_eq_prod_prod_Iio, Matrix.GeneralLinearGroup.coe_one, NumberField.InfinitePlace.ComplexEmbedding.conjugate_sign, Submodule.linearEquiv_det_reflection, Subgroup.HasDetOne.det_eq, HNNExtension.NormalWord.unitsSMul_one_group_smul, SpecialLinearGroup.centerEquivRootsOfUnity_symm_apply, val_eq_neg_one, Fin.sign_cycleIcc_of_le, SpecialLinearGroup.det_coe, Int.negOnePow_one, Equiv.Perm.mem_alternatingGroup, Equiv.Perm.ofSign_disjoint, Equiv.Perm.sign_of_pow_two_eq_one, NumberField.Units.coe_neg_one, ZMod.euler_criterion_units, Equiv.Perm.sign_refl, Int.negOnePow_odd, SpecialLinearGroup.coe_mul, Int.negOnePow_def, CategoryTheory.TwistShiftData.z_zero_left, NumberField.Units.torsion_eq_one_or_neg_one_of_odd_finrank, SpecialLinearGroup.coe_pow, Matrix.SpecialLinearGroup.toLin_equiv.symm_toLinearMap_eq, FiniteField.unit_isSquare_iff, WeierstrassCurve.VariableChange.one_def, Equiv.Perm.signAux3_mul_and_swap, CStarAlgebra.one_le_inv_iff_le_one, Matrix.SpecialLinearGroup.range_toGL, ComplexShape.Ξ΅_zero, Int.negOnePow_two_mul_add_one, divp_one, Complex.linearEquiv_det_conjAe, Int.units_eq_one_or, IsCyclotomicExtension.Rat.Three.Units.mem, SpecialLinearGroup.centerEquivRootsOfUnity_apply, Matrix.detp_smul_adjp, NumberField.Units.coe_one, units_eq_one, one_uzpow, Subgroup.HasDetPlusMinusOne.det_eq, Matrix.GeneralLinearGroup.map_mul_map_inv, linearEquiv_det_rotation, Matrix.detp_smul_add_adjp, Matrix.SpecialLinearGroup.coe_to_GLPos_to_GL_det, CategoryTheory.CatCenter.app_neg_one_zpow, ComplexShape.eulerCharSignsUpNat_Ο, Int.negOnePow_zero, eq_one, Int.units_sq, Matrix.isAddUnit_detp_smul_mul_adjp, Matrix.detp_mul, GradedTensorProduct.comm_coe_tmul_coe, MonoidWithZeroHom.inr_apply_unit, Polynomial.det_taylorLinearEquiv, UpperHalfPlane.det_J, val_one, Int.negOnePow_even, normUnit_one, TensorProduct.tmul_of_gradedMul_of_tmul, inv_eq_one_divp', HNNExtension.NormalWord.unitsSMulEquiv_symm_apply, IsCyclotomicExtension.Rat.Three.eq_one_or_neg_one_of_unit_of_congruent, Matrix.SpecialLinearGroup.toLin_equiv.toLinearMap_eq, UpperHalfPlane.denom_one, HNNExtension.toSubgroupEquiv_one, Matrix.mul_adjp_apply_ne, Matrix.det_neg_eq_smul, sign_finRotate, Equiv.Perm.IsCycle.sign, Equiv.Perm.IsThreeCycle.sign, IsUnit.unit_one, val_eq_one, Matrix.GeneralLinearGroup.map_one, Equiv.Perm.IsSwap.sign_eq, TensorProduct.gradedCommAux_lof_tmul, NumberField.Units.rootsOfUnity_eq_one, MonoidWithZeroHom.one_mem_valueMonoid, PowerSeries.invOneSubPow_val_one_eq_invUnitSub_one, Equiv.Perm.sign_one, Matrix.SpecialLinearGroup.det_mapGL, Matrix.UnitaryGroup.toGL_one, DirichletCharacter.Odd.toUnitHom_eval_neg_one, Module.Basis.orientation_neg_single, Equiv.Perm.sign_prod_list_swap, LinearEquiv.det_refl, Equiv.Perm.sign_of_cycleType', SpecialLinearGroup.baseChange_apply_coe, Polynomial.normUnit_X, CategoryTheory.CommShiftβSetup.z_zeroβ, CategoryTheory.CommShiftβSetup.int_Ξ΅, Equiv.Perm.ofSign_disjUnion, TensorProduct.gradedComm_of_tmul_of, SpecialLinearGroup.coe_div, Matrix.mul_adjp_add_detp, Valuation.IsRankOneDiscrete.exists_generator_lt_one, HNNExtension.NormalWord.unitsSMulEquiv_apply, CategoryTheory.CommShiftβSetup.z_zeroβ, Equiv.Perm.sign_swap', SpecialLinearGroup.coe_dualMap, Int.negOnePow_eq_one_iff, CStarAlgebra.inv_le_one_iff_one_le, Equiv.Perm.sign_swap, mk0_one, FiniteField.prod_univ_units_id_eq_neg_one, Matrix.isAddUnit_detp_mul_detp, SpecialLinearGroup.toLinearEquiv_to_linearMap, map_neg_one, MonoidWithZeroHom.inl_apply_unit, EqualCharZero.pnatCast_one, CategoryTheory.CommShiftβSetup.int_z, Int.units_mul_self, rootsOfUnity.eq_one, CategoryTheory.TwistShiftData.z_zero_right
|
instRepr π | CompOp | β |
inv π | CompOp | 11 mathmath: PowerSeries.invOneSubPow_inv_eq_one_sub_pow, RootPairing.Equiv.toEndUnit_inv, inv_val, inv_eq_val_inv, Module.End.isUnit_inv_apply_apply_of_isUnit, MulEquiv.val_inv_piUnits_apply, PowerSeries.invOneSubPow_inv_zero_eq_one, Module.End.isUnit_apply_inv_apply_of_isUnit, val_inv, HahnSeries.val_inv_toOrderTopSubOnePos_coe, MulEquiv.val_inv_piUnits_symm_apply
|
mkOfMulEqOne π | CompOp | 3 mathmath: ZMod.AddAutEquivUnits_apply, PowerSeries.invOneSubPow_eq_inv_one_sub_pow, val_mkOfMulEqOne
|
val π | CompOp | 888 mathmath: Set.center_units_subset, IsCyclotomicExtension.Rat.Three.eta_sq_add_eta_add_one, CircleDeg1Lift.units_inv_apply_apply, Polynomial.units_coeff_zero_smul, WeierstrassCurve.j_of_char_two, spectrum.inv_mem_iff, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply', WithZero.logOrderIso_apply, commute_iff_inv_mul_cancel, LaurentPolynomial.smeval_eq_sum, IsLocalization.mul_add_inv_left, Matrix.discr_conj, divp_sub, ContinuousLinearEquiv.unitsEquiv_apply, Polynomial.coe_normUnit_of_ne_zero, Polynomial.separable_X_pow_sub_C_unit, Matrix.GLPos.coe_neg_apply, OrderMonoidIso.val_inv_unitsWithZero_symm_apply, CommGroupWithZero.coe_normUnit, WithZero.val_expOrderIso_apply, min_val, Valuation.ltIdeal_le_leIdeal, Polynomial.Chebyshev.U_eval_zero, CircleDeg1Lift.translate_inv_apply, ClassGroup.mk0_integralRep, MulChar.eq_iff, commute_inv_coe, val_inv_unitsEquivProdSubtype_symm_apply, StandardEtalePair.inv_aeval_X_g, Matrix.GeneralLinearGroup.val_mkOfDetNeZero, Function.Antiperiodic.add_int_mul_eq, ModularForm.mul_slash, divp_eq_iff_mul_eq, CFC.inv_nonneg, autAdjoinRootXPowSubCEquiv_root, ext_iff, PadicInt.val_mkUnits, IsUnit.unit_inv_map, WithZero.withZeroUnitsEquiv_symm_apply_coe, Submonoid.val_mem_of_mem_units, FermatLastTheoremForThreeGen.Solution.lambda_sq_not_dvd_a_add_eta_sq_mul_b, AffineEquiv.coe_homothetyUnitsMulHom_eq_homothetyHom_coe, ZLattice.covolume_eq_det_inv, spectrum.invβ_mem_iff, Matrix.det_permute, WithZero.coe_unitsWithZeroEquiv_eq_units_val, val_inv_unitarySubgroupUnitsEquiv_symm_apply_coe, IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow, FermatLastTheoremForThreeGen.Solution.lambda_dvd_a_add_eta_sq_mul_b, isSMulRegular, nhds, FractionalIdeal.fg_unit, compare_val, Matrix.GeneralLinearGroup.mem_center_iff_val_mem_range_scalar, Representation.asGroupHom_apply, AbsoluteValue.map_units_intCast, IsCyclic.val_mulAutMulEquiv_apply, NNReal.exists_lt_of_strictMono, spectrum.units_smul_resolvent_self, AddAut.mulRight_symm_apply, Matrix.trace_units_conj, mul_inv_le_one, NormedRing.inverse_add_norm_diff_nth_order, Valuation.mem_ltIdeal_iff, WeierstrassCurve.variableChange_aβ, NumberField.mixedEmbedding.mem_idealLattice, cyclotomicCharacter.toZModPow, UpperHalfPlane.im_smul_eq_div_normSq, OrderMonoidIso.val_unitsCongr_symm_apply, Commute.units_inv_right_iff, NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_ne, NumberField.Units.regOfFamily_eq_det, Matrix.isHyperbolic_conj_iff, pinGroup.val_inv_toUnits_apply, ENNReal.mulRightOrderIso_symm_apply, Matrix.charpoly_units_conj', Set.unitEquivUnitsInteger_symm_apply_coe, Equiv.Perm.val_equivUnitsEnd_apply, CategoryTheory.Functor.commShiftβ_comm, val_unitarySubgroupUnitsEquiv_symm_apply_coe, Ideal.torsionMapQuot_apply, ValuationSubring.valuation_unit, IsPrimitiveRoot.val_toRootsOfUnity_coe, UpperHalfPlane.moebius_im, ModularForm.prod_slash, CommRing.Pic.mul_eq_tensor, ContinuousMap.val_unitsLift_apply_apply, rootsOfUnity.integer_power_of_ringEquiv, mem_principal_ideals_iff, IsUnit.mul_val_inv, OnePoint.smul_infty_eq_self_iff, Matrix.GeneralLinearGroup.coe_toLin, IsLocalizedModule.iso_apply_mk, normUnit_mul_normUnit, PadicInt.norm_units, CategoryTheory.CatCenter.smul_iso_inv_eq', IsCyclotomicExtension.Rat.Three.coe_eta, WithZeroTopology.nhds_zero_of_units, NumberField.Units.pos_at_place, LaurentPolynomial.smeval_T_pow, divp_add, toMatrix_rotation, irreducible_mul_units, Polynomial.Chebyshev.T_eval_zero, ModularForm.prod_slash_sum_weights, MonoidHom.toHomPerm_apply_symm_apply, IsPrimitiveRoot.pow_sub_one_eq_geom_sum_mul_geom_sum_inv_mul_pow_sub_one, Matrix.isHyperbolic_conj'_iff, ModularGroup.coe_apply_complex, Function.Antiperiodic.sub_int_mul_eq, MulChar.one_apply_coe, LinearMap.GeneralLinearGroup.generalLinearEquiv_to_linearMap, WeierstrassCurve.j_of_char_three, FermatLastTheoremForThreeGen.Solution'.H, Matrix.isElliptic_conj'_iff, WithZero.coe_expEquiv_apply, coe_neg_one, PreQuasiregular.add_inv_add_mul_eq_zero, MulEquiv.val_piUnits_symm_apply, Complex.conj_rootsOfUnity, val_unitsCentralizerEquiv_apply_coe, Complex.mem_rootsOfUnity, NumberField.Units.coe_mul, FermatLastTheoremForThreeGen.Solution.a_add_eta_mul_b, mem_rootsOfUnity_iff_mem_nthRoots, Subgroup.unit_of_mem_ofUnits_spec_val_eq_of_mem, modularCyclotomicCharacter.spec, Matrix.det_units_conj', rootsOfUnity.coe_injective, isOfFinOrder_val, Polynomial.Chebyshev.T_eval_two_mul_zero, PreQuasiregular.inv_add_add_mul_eq_zero, Equiv.Perm.prod_Ioi_comp_eq_sign_mul_prod, LaurentPolynomial.evalβ_C_mul_T, Matrix.coe_units_inv, modularCyclotomicCharacter.toFun_spec', LocalizedModule.lift'_mk, HNNExtension.NormalWord.prod_cons, Valuation.unit_map_eq, val_inv_eq_inv_val, orderOf_units, associated_mul_unit_right_iff, affineSpan_eq_affineSpan_lineMap_units, inv_le_one, CategoryTheory.CatCenter.smul_iso_inv_eq'_assoc, Polynomial.Chebyshev.T_eval_neg, Asymptotics.isBigOWith_self_const_mul', inv_val, unitsEquivProdSubtype_apply_coe, val_unitsCenterToCenterUnits_apply_coe, ContinuousLinearEquiv.unitsEquivAut_apply, NormalizationMonoid.normUnit_coe_units, val_inv_inj, IsUnit.unit_map, WithZero.expOrderIso_symm_apply, PowerSeries.IsWeierstrassFactorization.isWeierstrassDivision, Matrix.isParabolic_conj'_iff, associated_unit_mul_right_iff, coe_map, pinGroup.val_toUnits_apply, Valued.is_topological_valuation, inv_eq_val_inv, continuous_val, Subgroup.mem_ofUnits_iff, divp_self, MonoidWithZeroHom.one_apply_val_unit, spinGroup.val_inv_toUnits_apply, mul_inv_mem_unitary, Matrix.GeneralLinearGroup.val_mk'', OrderMonoidIso.val_unitsCongr_apply, DirichletCharacter.unit_norm_eq_one, hasFDerivAt_ringInverse, CategoryTheory.Aut.toEnd_apply, mul_inv_eq_iff_eq_mul, rootsOfUnity.val_mkOfPowEq_coe, CircleDeg1Lift.coe_toOrderIso_symm, Polynomial.Chebyshev.U_eval_neg_one, CircleDeg1Lift.translate_iterate, unitarySubgroupUnitsEquiv_apply_coe, OnePoint.smul_some_eq_ite, coe_dvd, coe_prod, instInvertibleCarrierOutSemimoduleCatValSkeleton, IsPrimitiveRoot.coe_autToPow_apply, WeierstrassCurve.variableChange_bβ, Matrix.isUnits_det_units, Submonoid.coe_inv_val_mul_coe_val, val_toUnits_apply, conj_pow', PowerSeries.coeff_invOfUnit, Subgroup.exists_mem_ofUnits_val_eq, NumberField.Units.regulator_eq_det, Int.cast_negOnePow, CircleDeg1Lift.coe_toOrderIso_inv, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, OrderMonoidIso.val_inv_unitsCongr_symm_apply, orderEmbeddingVal_apply, divp_mul_cancel, unitSphereToUnits_apply_coe, ZMod.dft_comp_unitMul, WeierstrassCurve.coe_map_Ξ', inv_mul, WeierstrassCurve.VariableChange.mul_def, coe_toPrincipalIdeal, NumberField.Units.coe_coe, units_smul_eq_self_iff, MvPowerSeries.constantCoeff_invOfUnit, OrderMonoidIso.withZeroUnits_apply, mul_right_dvd, CommRing.Pic.inv_eq_dual, units_smul_eq_neg_iff, Module.End.algebraMap_isUnit_inv_apply_eq_iff', spectrum.resolvent_eq, NumberField.Units.finrank_mul_regOfFamily_eq_det, Equiv.Perm.sign_abs, Valuation.mem_unitGroup_iff, HNNExtension.NormalWord.prod_unitsSMul, Submonoid.coe_val_mul_coe_inv_val, NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis, val_inv_unitsNonZeroDivisorsEquiv_symm_apply_coe, MulChar.equivToUnitHom_symm_coe, fderiv_inverse, Algebra.SubmersivePresentation.jacobianRelations_spec, NumberField.det_basisOfFractionalIdeal_eq_absNorm, coe_map_inv, CircleDeg1Lift.units_apply_inv_apply, OrderMonoidIso.val_unitsWithZero_symm_apply, DihedralGroup.oddCommuteEquiv_symm_apply, coe_star, coe_smul, CommRing.Pic.mk_eq_iff, divp_add_divp, mul_inv_eq_mul_inv_iff, Module.Basis.det_unitsSMul, val_set_image_rootsOfUnity_one, IsStarNormal.val_inv, CommMonCat.val_units_map_hom_apply, LaurentPolynomial.evalβ_T, FiniteField.sum_subgroup_units_eq_zero, Submonoid.val_inv_unitsTypeEquivIsUnitSubmonoid_symm_apply, Nonneg.val_unitsEquivPos_symm_apply_coe, Polynomial.roots_C_mul_X_sub_C_of_IsUnit, CommRing.Pic.mk_eq_self, NumberField.Units.norm, WeierstrassCurve.variableChange_bβ, LaurentSeries.exists_ratFunc_val_lt, MonoidWithZeroHom.valueGroup_eq_range, AffineEquiv.coe_homothetyUnitsMulHom_apply_symm, NumberField.mixedEmbedding.span_idealLatticeBasis, MulChar.pow_apply_coe, Valued.hasBasis_nhds_zero, CommMonCat.val_inv_units_map_hom_apply, PowerSeries.constantCoeff_invOfUnit, Algebra.SubmersivePresentation.map_invJacobianOfHasCoeffs, IsDiscreteValuationRing.addVal_def', WeierstrassCurve.variableChange_bβ, mulRight_bijective, modularCyclotomicCharacter.toFun_spec, CategoryTheory.TwistShiftData.shift_z_app, ZMod.inv_coe_unit, Nonneg.val_unitsHomeomorphPos_symm_apply_coe, DirichletCharacter.toUnitHom_eq_char', IsCyclic.val_inv_mulAutMulEquiv_apply, MulChar.apply_mem_rootsOfUnity_of_pow_eq_one, IsValuativeTopology.mem_nhds_iff', Matrix.GeneralLinearGroup.coe_one, ContinuousLinearEquiv.symm_smul_apply, MulEquiv.restrictRootsOfUnity_coe_apply, WeierstrassCurve.VariableChange.inv_def, FractionalIdeal.canonicalEquiv_mk0, CommRing.Pic.mapAlgebra_apply, Matrix.GeneralLinearGroup.val_mk', Matrix.det_permutation, CommRing.Pic.ext_iff, IsOpenUnits.isOpenEmbedding_unitsVal, Valuation.IsUniformizer.val, val_le_val, NumberField.mixedEmbedding.unit_smul_eq_iff_mul_eq, ValuativeRel.exists_valuation_posSubmonoid_div_valuation_posSubmonoid_eq, ValuationSubring.coe_unitGroupMulEquiv_apply, ContinuousMap.val_unitsLift_symm_apply_apply, Submonoid.LocalizationMap.inv_unique, mul_inv_cancel_right, MulChar.eq_one_iff, CommRing.Pic.instFreeAsModuleOfNat, MonoidHom.coe_toHomUnits, Matrix.isParabolic_conj_iff, ConjAct.units_smul_def, AffineEquiv.val_equivUnitsAffineMap_apply, val_set_image_rootsOfUnity, spectrum.units_conjugate, spectrum.zero_mem_resolventSet_of_unit, continuousOn_zpowβ_spectrum, MulEquiv.val_inv_piUnits_apply, NumberField.Units.dirichletUnitTheorem.sum_logEmbedding_component, Matrix.GeneralLinearGroup.fixpointPolynomial_eq_zero_iff, LaurentSeries.exists_Polynomial_intValuation_lt, IsPrimitiveRoot.coe_units_iff, CategoryTheory.CatCenter.smul_iso_hom_eq'_assoc, IsLocalization.lift_mk', IsUnit.coe_liftRight, Matrix.GeneralLinearGroup.toLin'_apply, ValuationSubring.mem_unitGroup_iff, val_cfcUnits, Submonoid.unitsTypeEquivIsUnitSubmonoid_apply_coe, mul_inv_le_iff, multiplicity_of_unit_right, NumberField.mixedEmbedding.covolume_idealLattice, val_zpow_eq_zpow_val, dvd_mul_left, one_le_inv, Nonneg.val_inv_unitsHomeomorphPos_symm_apply_coe, gaussSum_aux_of_mulShift, quadraticChar_exists_neg_one', IsLocalizedModule.fromLocalizedModule_mk, Commute.units_val, mem_posSubgroup, Unitization.val_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, Function.Antiperiodic.add_zsmul_eq, OrderMonoidIso.unitsWithZero_apply, NumberField.Units.mem_torsion, WithZero.val_inv_expOrderIso_apply, Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, map_rootsOfUnity_eq_pow_self, val_unitsNonZeroDivisorsEquiv_symm_apply_coe, WeierstrassCurve.variableChange_def, val_eq_neg_one, spectrum.invβ_mem_inv_iff, commute_iff_inv_mul_cancel_assoc, Subgroup.val_centerUnitsEquivUnitsCenter_symm_apply_coe, IsUnit.mul_liftRight_inv, Commute.units_inv_left_iff, mul_inv, inv_pos, val_inv_ofPowEqOne, Matrix.det_reindex, IsValuativeTopology.mem_nhds_zero_iff, normalize_apply, PowerSeries.invUnitsSub_mul_sub, ContinuousMap.unitsLift_apply_inv_apply, mul_left_dvd, groupCohomology.norm_ofAlgebraAutOnUnits_eq, Submodule.projective_units, WittVector.exists_eq_pow_p_mul', CStarAlgebra.inv_le_one, WeierstrassCurve.variableChange_aβ, IsCyclotomicExtension.Rat.Three.eta_sq, NumberField.Units.coe_neg_one, Valuation.IsRankOneDiscrete.generator_zpowers_eq_range, WeierstrassCurve.variableChange_aβ, mul_divp_cancel, inv_mul_le_iff, Matrix.GeneralLinearGroup.ext_iff, ENNReal.mulLeftOrderIso_symm_apply, max_val, FiniteField.sum_subgroup_pow_eq_zero, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, NumberField.mixedEmbedding.logMap_eq_logEmbedding, Matrix.isElliptic_conj_iff, OrderMonoidIso.val_inv_unitsCongr_apply, val_div_eq_div_val, MonoidWithZeroHom.inl_mul_inr_eq_mk_of_unit, WeierstrassCurve.variableChange_cβ, Submonoid.LocalizationMap.lift_mk', inv_pow_eq_pow_inv, groupCohomology.exists_div_of_norm_eq_one, Set.val_unitEquivUnitsInteger_apply_coe, commute_coe_inv, quasispectrum.mem_of_not_quasiregular, unitary.val_toUnits_apply, IsCyclotomicExtension.Rat.galEquivZMod_apply_of_pow_eq, PowerSeries.one_sub_pow_add_mul_invOneSubPow_val_eq_one_sub_pow, NormedRing.inverse_add, Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_apply, mul_right_eq_zero, Matrix.val_planeConformalMatrix, divp_eq_div, coe_unop_opEquiv, Matrix.UnitaryGroup.coe_toGL, Valuation.Integers.valuation_unit, divp_eq_one_iff_eq, rootsOfUnity.coe_mkOfPowEq, toAut_hom, CircleDeg1Lift.translate_apply, NumberField.Units.dirichletUnitTheorem.mult_log_place_eq_zero, Nonneg.unitsHomeomorphPos_apply_coe, val_mk, NormedRing.inverse_one_sub, NormedRing.inverse_add_norm, Submodule.unitsToPic_apply, PowerSeries.one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val, mul_eq_one_iff_eq_inv, Valued.closure_coe_completion_v_lt, Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval, WithZeroTopology.nhds_coe_units, AffineEquiv.equivUnitsAffineMap_symm_apply_apply, NumberField.Units.dirichletUnitTheorem.log_le_of_logEmbedding_le, normalize_coe_units, NormedSpace.exp_units_conj', WeierstrassCurve.coe_inv_variableChange_Ξ', CategoryTheory.Functor.CommShiftβ.comm, val_unitsEquivProdSubtype_symm_apply, Valued.cauchy_iff, pinGroup.units_mem_iff, Matrix.nonsing_inv_apply, Nonneg.unitsEquivPos_apply_coe, ValuationSubring.valuation_eq_iff, ZMod.val_coe_unit_coprime, map_units_inv, Function.Antiperiodic.zsmul_sub_eq, inv_mul_eq_one, mul_inv_eq_one, NormedRing.inverse_add_norm_diff_second_order, HahnSeries.binomial_power, nnnorm_pos, val_inj, LaurentPolynomial.evalβ_C_mul_T_neg_n, Matrix.charpoly_units_conj, val_unitsCentralizerEquiv_symm_apply_coe, mul_inv', mul_inv_cancel_left, Subgroup.val_centerUnitsEquivUnitsCenter_apply_coe, ContinuousLinearEquiv.unitsEquivAut_symm_apply, val_neg, NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt, IsValuativeTopology.hasBasis_nhds, one_divp, Int.abs_negOnePow, AlgEquiv.algHomUnitsEquiv_apply_symm_apply, AddConstEquiv.coe_val_inv_equivUnits_apply, continuous_iff, Polynomial.Chebyshev.U_eval_two_mul_zero, AlgEquiv.val_algHomUnitsEquiv_symm_apply, CircleDeg1Lift.coe_toOrderIso, CategoryTheory.CatCenter.smul_iso_inv_eq_assoc, abs_unit_intCast, HomologicalComplex.eulerChar_eq_sum_finSet_of_finrankSupport_subset, NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le, Unitary.val_toUnits_apply, Ring.inverse_unit, val_smul, IsValuativeTopology.hasBasis_nhds_zero, WeierstrassCurve.variableChange_Ξ, Int.units_natAbs, NumberField.Units.complexEmbedding_apply, ContinuousLinearEquiv.unitsEquivAut_apply_symm, EqualCharZero.pnatCast_eq_natCast, OnePoint.smul_infty_eq_ite, ClassGroup.mk_eq_one_iff, NumberField.fractionalIdeal_rank, WeierstrassCurve.coe_inv_map_Ξ', Valuation.mem_ltAddSubgroup_iff, WeierstrassCurve.variableChange_aβ, val_inv_cfcUnits, AddAut.mulRight_apply, isGroupLikeElem_unitsInv, exists0', toPrincipalIdeal_eq_iff, Matrix.GeneralLinearGroup.mem_center_iff_val_eq_scalar, NumberField.Units.coe_pow, embedding_val_mk, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, mulLeft_apply, LucasLehmer.ΟUnit_coe, LinearEquiv.smul_apply, Associates.coe_unit_eq_one, AffineEquiv.equivUnitsAffineMap_symm_apply_symm_apply, Set.unit_valuation_eq_one, NumberField.Units.abs_det_eq_abs_det, unitsEquivNeZero_apply_coe, LaurentPolynomial.evalβ_toLaurent, isEmbedding_val, coe_inv_smul, GroupLike.val_toUnits_apply, LinearEquiv.toLinearMap_smul, Unitary.val_inv_toUnits_apply, topology_eq_inf, hasStrictFDerivAt_ringInverse, Submonoid.inv_val_mem_of_mem_units, AddConstEquiv.equivUnits_symm_apply_apply, Matrix.GeneralLinearGroup.coe_inv, Valuation.ltSubmodule_le_leSubmodule, NumberField.Units.coe_injective, NumberField.Units.coe_one, WithZero.logEquiv_apply, Valued.integer.norm_unit, Matrix.discr_conj', spectrum.map_inv, LocalizedModule.lift_mk, Valuation.ltAddSubgroup_le_leAddSubgroup, LinearMap.GeneralLinearGroup.coe_ofLinearEquiv, NumberField.IsCMField.mem_realUnits_iff, PowerSeries.Unit_of_divided_by_X_pow_order_nonzero, CategoryTheory.CatCenter.smul_iso_hom_eq_assoc, IsUnit.val_subInvSMul, isOpenUnits_iff, NumberField.mixedEmbedding.unitSMul_smul, conj_pow, ContinuousMap.canLift, ZMod.unitsMap_val, AffineEquiv.equivUnitsAffineMap_symm_apply_toFun, emultiplicity_of_unit_right, unit_associated_one, Matrix.exp_units_conj', Submonoid.LocalizationMap.lift_apply, smul_def, Int.units_coe_mul_self, Polynomial.Chebyshev.U_eval_neg, inv_mul_eq_inv_mul_iff, WeierstrassCurve.coe_Ξ', ValuationSubring.principalUnitGroupEquiv_apply, Algebra.SubmersivePresentation.aeval_invJacobianOfHasCoeffs, MonCat.val_units_map_hom_apply, Irreducible.not_dvd_unit, Submonoid.mem_units_iff, LinearMap.GeneralLinearGroup.coe_toLinearEquiv, Module.Basis.det_inv, Matrix.GeneralLinearGroup.val_inv_det_apply, Submodule.instInvertibleSubtypeMemVal, IsUnit.val_inv_unit', Polynomial.coeff_inv_units, Polynomial.Chebyshev.C_eval_neg_two, lcm_units_coe_left, Matrix.SpecialLinearGroup.coe_GL_coe_matrix, NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt', MonoidWithZeroHom.fst_apply_coe, Ideal.rootsOfUnityMapQuot_apply, LaurentPolynomial.smeval_single, eq_mul_inv_iff_mul_eq, CircleDeg1Lift.translationNumber_conj_eq, irreducible_units_mul, Matrix.SpecialLinearGroup.eq_scalar_center_equiv_rootsOfUnity, associated_unit_mul_left_iff, Valued.mem_nhds_zero, isUnit_mul_units, Polynomial.Chebyshev.T_eval_zero_of_even, Matrix.GeneralLinearGroup.coe_map_mul_map_inv, CategoryTheory.CatCenter.smul_iso_inv_eq, val_set_image_rootsOfUnity_two, ValuationSubring.mem_principalUnitGroup_iff, add_eq_mul_one_add_div, Valued.mem_nhds, CategoryTheory.CatCenter.app_neg_one_zpow, Commute.units_val_iff, dvd_mul_right, OnePoint.smul_infty_def, Int.coe_negOnePow_natCast, inv_mul_cancel_right, Polynomial.newtonMap_apply_of_isUnit, IsDedekindDomain.HeightOneSpectrum.valuationOfNeZero_eq, Matrix.det_mul_aux, NumberField.Units.dirichletUnitTheorem.logEmbedding_component, NumberField.Units.coe_zpow, NumberField.mem_span_basisOfFractionalIdeal, MonoidWithZeroHom.valueMonoid_eq_closure, continuousOn_invβ_spectrum, zero_notMem_spectrum, Algebra.SubmersivePresentation.exists_sum_eq_Ο_jacobian_mul_Ο_jacobian_inv_sub_one, exists_iff_ne_zero, Matrix.GeneralLinearGroup.val_inv_scalar_apply, spectrum.units_conjugate', Int.nnnorm_coe_units, AbsoluteValue.map_units_int, SemiconjBy.units_inv_symm_left_iff, Asymptotics.IsBigOWith.const_mul_right', AffineEquiv.coe_homothetyUnitsMulHom_apply, Matrix.det_permute', FiniteField.sum_pow_units, cyclotomicCharacter.toZModPow_toFun, ValuationSubring.coe_unitGroupMulEquiv_symm_apply, MonoidWithZeroHom.inr_apply_unit, Matrix.mem_glpos, AlgEquiv.val_inv_algHomUnitsEquiv_symm_apply, PowerSeries.invOneSubPow_val_eq_mk_sub_one_add_choose_of_pos, continuous_coe_inv, MvPowerSeries.coeff_invOfUnit, Valuation.exists_pow_Uniformizer, Matrix.disc_conj, CategoryTheory.TwistShiftData.shiftFunctorAdd'_inv_app, Matrix.GeneralLinearGroup.val_map_apply, LaurentPolynomial.evalβ_T_neg_n, Submodule.span_singleton_eq_one_iff, Polynomial.coe_normUnit, MulChar.ofRootOfUnity_spec, val_one, isEmbedding_valβ, val_injective, toAut_inv, val_oneSub, PowerSeries.heval_unit, inv_neg, CategoryTheory.CatCenter.smul_iso_hom_eq', exists_pow_ltβ, Complex.norm_eq_one_of_mem_rootsOfUnity, sub_divp, PowerSeries.IsWeierstrassDivision.isWeierstrassFactorization, divp_inv, coeHom_apply, isUnit_units_mul, lipschitzGroup.coe_mem_iff_mem, Equiv.Perm.equivUnitsEnd_symm_apply_symm_apply, commute_iff_mul_inv_cancel_assoc, NormedRing.inverse_add_norm_diff_first_order, Submonoid.LocalizationMap.mul_inv_right, IsDiscreteValuationRing.addVal_eq_zero_of_unit, cyclotomicCharacter.spec, inv_eq_one_divp', CategoryTheory.TwistShiftData.shiftFunctorAdd'_hom_app, val_unitOfInvertible, inv_eq_one_divp, GroupLike.val_inv_toUnits_apply, MonoidWithZeroHom.mem_valueGroup_iff_of_comm, MonCat.val_inv_units_map_hom_apply, Matrix.GeneralLinearGroup.val_swap, toUnits_symm_apply, coe_opEquiv_symm, spectrum.unit_mem_mul_comm, WithZeroTopology.tendsto_units, Module.End.ker_aeval_ring_hom'_unit_polynomial, OrderIso.withZeroUnits_apply, ModularForm.prod_fintype_slash, Subgroup.val_mem_ofUnits_iff_mem, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, Matrix.SpecialLinearGroup.coe_GLPos_coe_GL_coe_matrix, mulLeft_bijective, Set.subset_center_units, ContinuousLinearEquiv.smul_apply, nnnorm_commutator_units_sub_one_le, rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar_val, IsUnit.val_inv_subInvSMul, Matrix.GeneralLinearGroup.map_apply, WeierstrassCurve.coe_variableChange_Ξ', PadicInt.mkUnits_eq, nonZeroDivisorsEquivUnits_symm_apply_coe, Set.center_units_eq, NormedRing.inverse_continuousAt, UpperHalfPlane.val_J, Valuation.IsUniformizer.iff, LinearEquiv.coe_inv_det, submodule_isFractional, IsLocalizedModule.fromLocalizedModule'_mk, Valued.hasBasis_uniformity, ModularForm.slash_def, rootsOfUnityEquivNthRoots_apply, MulChar.trivial_apply, Valuation.mem_ltSubmodule_iff, Equiv.Perm.equivUnitsEnd_symm_apply_apply, rootsOfUnityCircleEquiv_apply, one_le_mul_inv, toUnits_val_apply, spectrum.preimage_units_mul_comm, one_le_inv_mul, rootsOfUnity.integer_power_of_ringEquiv', ArithmeticFunction.inv_zetaUnit, Int.norm_coe_units, IsPrimitiveRoot.autToPow_spec, LaurentPolynomial.smeval_C_mul_T_n, ZMod.isUnit_cast_of_dvd, Submonoid.LocalizationMap.mul_inv_left, MulChar.coe_toUnitHom, ZMod.coe_unitOfCoprime, norm_commutator_units_sub_one_le, le_inv_mul_iff, contDiffAt_ringInverse, toPrincipalIdeal_def, SpecialLinearGroup.coe_toGeneralLinearGroup_apply, NumberField.basisOfFractionalIdeal_apply, contMDiff_val, val_eq_one, IsOfFinOrder.val_inv_unit, modularCyclotomicCharacter'.spec', instCanLiftUnitsValIsUnit, Polynomial.natDegree_coe_units, Matrix.SpecialLinearGroup.mapGL_coe_matrix, AffineEquiv.val_inv_equivUnitsAffineMap_apply, LinearMap.trace_conj, IsUnit.val_inv_apply, coe_star_inv, HahnSeries.coeff_toOrderTopSubOnePos_pow, SemiconjBy.units_val_iff, isUnit, FiniteMultiplicity.not_of_unit_left, Valuation.coe_ltAddSubgroup, PowerSeries.invOneSubPow_val_one_eq_invUnitSub_one, Matrix.GeneralLinearGroup.coe_mul, CircleDeg1Lift.translationNumber_conj_eq', AddConstEquiv.equivUnits_symm_apply_symm_apply, val_pow_eq_pow_val, rootsOfUnity.coe_pow, restrictRootsOfUnity_coe_apply, Matrix.det_units_conj, LinearEquiv.symm_smul_apply, norm_pos, MulChar.ext_iff, CircleDeg1Lift.translationNumber_translate, Polynomial.Chebyshev.one_lt_negOnePow_mul_eval_T_real, LaurentPolynomial.evalβ_T_n, isRegular, MulChar.ofUnitHom_coe, ZMod.coe_unitOfIsCoprime, Subgroup.HasDetPlusMinusOne.abs_det, val_lt_val, IsPrimitiveRoot.val_inv_toRootsOfUnity_coe, mem_rootsOfUnity', Matrix.disc_conj', CircleDeg1Lift.translationNumber_units_inv, mul_right_inj, MonoidWithZeroHom.mem_valueMonoid_iff, Polynomial.Chebyshev.one_le_negOnePow_mul_eval_T_real, Polynomial.Chebyshev.T_eval_neg_one, NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr, le_mul_inv_iff, Submonoid.LocalizationMap.mul_inv, ContinuousMap.unitsLift_symm_apply_apply_inv', mulLECancellable_val, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, associated_mul_unit_left_iff, Matrix.trace_units_conj', SlashInvariantForm.slash_action_eqn', divp_sub_divp, Matrix.det_apply', Lagrange.nodal_subgroup_eq_X_pow_card_sub_one, ModularGroup.det_coe, FiniteField.sum_subgroup_units, PowerSeries.invUnitsSub_mul_X, CategoryTheory.TwistShiftData.commShift, inv_mul_eq_iff_eq_mul, val_mk0, WithZero.withZeroUnitsEquiv_apply, NormedRing.inverse_add_nth_order, Module.Basis.det_unitsSMul_self, Matrix.GeneralLinearGroup.val_inv_swap, zero_lt, Submonoid.LocalizationMap.liftβ_apply, MulChar.apply_mem_rootsOfUnity_orderOf, FermatLastTheoremForThreeGen.a_cube_add_b_cube_eq_mul, lipschitzGroup.involute_act_ΞΉ_mem_range_ΞΉ, mul_left_inj, NumberField.Units.finrank_mul_regulator_eq_det, IsUnit.val_inv_mul, IsCyclotomicExtension.Rat.Three.cube_sub_one_eq_mul, Nonneg.val_inv_unitsEquivPos_symm_apply_coe, GradedObject.eulerChar_eq_sum_finSet_of_finrankSupport_subset, Matrix.GeneralLinearGroup.val_scalar_apply, val_rootsOfUnityEquivOfPrimitiveRoots_apply_coe, mul_left_eq_zero, MonoidWithZeroHom.snd_apply_coe, IsUnit.liftRight_inv_mul, NumberField.instIsLocalizedModuleIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmoduleValFractionalIdealNonZeroDivisorsRestrictScalarsSubtype, WeierstrassCurve.Affine.CoordinateRing.XYIdeal'_eq, NumberField.Units.sum_mult_mul_log, Submonoid.val_unitsTypeEquivIsUnitSubmonoid_symm_apply, val_inv, MulEquiv.val_piUnits_apply, WithZeroTopology.singleton_mem_nhds_of_units, PadicInt.unitCoeff_spec, Valued.integer.norm_coe_unit, lcm_units_coe_right, Submonoid.IsUnit.Submonoid.coe_inv, MulChar.coe_equivToUnitHom, GroupWithZero.eq_zero_or_unit, invOf_units, Matrix.GeneralLinearGroup.coe_map_inv_mul_map, Polynomial.Chebyshev.S_eval_neg_two, AffineIndependent.units_lineMap, Matrix.exp_units_conj, isOpenEmbedding_val, Unitization.val_unitsFstOne_mulEquiv_quasiregular_apply, NormedSpace.exp_units_conj, FermatLastTheoremForThreeGen.Solution.lambda_sq_not_dvd_a_add_eta_mul_b, IsUnit.unit_spec, instInvertibleCarrierOutModuleCatValSkeleton, SemiconjBy.units_val, CategoryTheory.CatCenter.smul_iso_hom_eq, val_ofPowEqOne, PowerSeries.IsWeierstrassDivisorAt.seq_one, autAdjoinRootXPowSubC_root, Matrix.rank_unit, IsValuativeTopology.mem_nhds_iff, LaurentPolynomial.evalβ_C_mul_T_n, CategoryTheory.Functor.commShiftβ_comm_assoc, PowerSeries.rescale_neg_one_invOneSubPow, Subgroup.mem_units_iff_val_mem, NumberField.Units.dirichletUnitTheorem.exists_unit, PadicInt.unitCoeff_coe, Equiv.Perm.prod_Iio_comp_eq_sign_mul_prod, Function.Antiperiodic.int_mul_sub_eq, SemiconjBy.units_inv_right_iff, divp_eq_divp_iff, Valued.exists_pow_lt_of_le_exp_neg_one, Polynomial.roots_C_mul_X_add_C_of_IsUnit, HahnSeries.val_toOrderTopSubOnePos_coe, WeierstrassCurve.variableChange_cβ, HahnSeries.mem_orderTopSubOnePos_iff, rootsOfUnityEquivNthRoots_symm_apply, IsDiscreteValuationRing.eq_unit_mul_pow_irreducible, IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroToFun_eq, Equiv.Perm.val_inv_equivUnitsEnd_apply, HahnSeries.val_inv_toOrderTopSubOnePos_coe, mk0_val, Unitization.unitsFstOne_val_val_fst, Real.exists_lt_of_strictMono, IsUnit.val_unit', commute_iff_mul_inv_cancel, Ring.inverse_of_isUnit, LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv, IsOfFinOrder.val_unit, NumberField.mixedEmbedding.norm_unit, WeierstrassCurve.variableChange_aβ, Module.Basis.toMatrix_unitsSMul, eq_inv_mul_iff_mul_eq, mulRight_apply, UpperHalfPlane.c_mul_im_sq_le_normSq_denom, WithZero.val_logOrderIso_symm_apply, HNNExtension.NormalWord.t_pow_smul_eq_unitsSMul, NumberField.IsCMField.complexConj_torsion, isOpenMap_val, AddConstEquiv.coe_val_equivUnits_apply, DirichletCharacter.changeLevel_eq_cast_of_dvd, rootsOfUnityEquivOfPrimitiveRoots_symm_apply, analyticAt_inverse, inv_mul', UpperHalfPlane.smulAux'_im, Matrix.coe_units_zpow, FractionalIdeal.coe_mk0, PowerSeries.derivative_inv, val_mul, ValuationSubring.coe_unitGroupToResidueFieldUnits_apply, FermatLastTheoremForThreeGen.ex_cube_add_cube_eq_and_isCoprime_and_not_dvd_and_dvd, inv_mul_le_one, ArithmeticFunction.coe_zetaUnit, modularCyclotomicCharacter.aux_spec, val_mkOfMulEqOne, Int.cast_negOnePow_natCast, HomologicalComplex.homologyEulerChar_eq_sum_finSet_of_finrankSupport_subset, mk_semiconjBy, Module.End.algebraMap_isUnit_inv_apply_eq_iff, ZMod.rootsOfUnityAddChar_val, FermatLastTheoremForThreeGen.Solution.lambda_dvd_a_add_eta_mul_b, val_div_eq_divp, Valuation.IsRankOneDiscrete.generator_mem_range, WithZero.val_inv_logOrderIso_symm_apply, PowerSeries.invOneSubPow_val_succ_eq_mk_add_choose, NumberField.IsCMField.Units.complexConj_eq_self_iff, coe_mapEquiv, AffineEquiv.equivUnitsAffineMap_symm_apply_invFun, NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_ne, Valuation.exists_div_eq_of_surjective, CircleDeg1Lift.translationNumber_zpow, IsCyclotomicExtension.autEquivPow_symm_apply, Unitization.mem_unitsFstOne, WithZero.unitsWithZeroEquiv_apply, AlgEquiv.algHomUnitsEquiv_apply_apply, mul_eq_one_iff_inv_eq, cyclotomicCharacter.toFun_spec, MonoidWithZeroHom.inl_apply_unit, Matrix.GeneralLinearGroup.toLin_apply, inv_mul_mem_unitary, Polynomial.degree_coe_units, Unitization.unitsFstOne_val_inv_val_fst, ValuationSubring.principalUnitGroup_symm_apply, Subgroup.hasDetPlusMinusOne_iff_abs_det, RootPairing.Equiv.toEndUnit_val, embedProduct_apply, Submodule.fg_unit, IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow', LinearEquiv.coe_det, eq_divp_iff_mul_eq, val_inv_unitOfInvertible, Polynomial.Chebyshev.U_eval_zero_of_even, Polynomial.Chebyshev.eval_T_real_cos_int_mul_pi_div, MulEquiv.val_inv_piUnits_symm_apply, WithZeroTopology.hasBasis_nhds_units, add_divp, chartAt_apply, spinGroup.val_toUnits_apply, IsCyclotomicExtension.Rat.galEquivZMod_smul_of_pow_eq, ModularForm.slash_apply, Function.Antiperiodic.sub_zsmul_eq, Matrix.GLPos.coe_neg, inv_mul_cancel_left, IsCyclotomicExtension.Rat.Three.lambda_dvd_mul_sub_one_mul_sub_eta_add_one, FermatLastTheoremForThreeGen.lambda_sq_dvd_or_dvd_or_dvd, gaussSum_mulShift, Matrix.GeneralLinearGroup.val_det_apply, UpperHalfPlane.petersson_slash, WeierstrassCurve.variableChange_bβ, Matrix.GeneralLinearGroup.fin_two_smul_prod
|
| Name | Category | Theorems |
|---|
AddUnits π | CompData | 218 mathmath: val_toAddUnits_apply, AddSubgroup.ofAddUnits_right_inverse, AddUnits.orderEmbeddingVal_apply, AddUnits.map_mk, AddSemiconjBy.addUnits_val_iff, AddSubgroup.ofAddUnits_bot, AddUnits.vadd_def, AddSubmonoid.coe_val_add_coe_neg_val, IsAddUnit.addUnit_nsmul, AddSubmonoid.LocalizationMap.add_neg_right, AddUnits.isOfFinAddOrder_val, AddUnits.embedProduct_injective, AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid_apply_coe, AddSubmonoid.addUnit_mem_leftNeg, ofAddUnits_addUnits_gc, AddSubmonoid.addUnits_iInfβ, AddUnits.addCommute_iff_neg_add_cancel_assoc, IsAddUnit.add_val_neg, AddSubmonoid.val_neg_addUnitsTypeEquivIsAddUnitAddSubmonoid_symm_apply, AddUnits.instAddArchimedean, AddEquiv.val_neg_piAddUnits_apply, AddSemiconjBy.addUnits_neg_right, AddUnits.neg_eq_of_add_eq_zero_left, AddSubmonoid.addUnits_sInf, AddUnits.coeHom_apply, AddUnits.add_neg_eq_add_neg_iff, AddUnits.coe_unop_opEquiv, AddSubgroup.mem_iff_toAddUnits_mem_addUnits, Subsingleton.addUnits_of_isAddUnit, addOrderOf_addUnits, IsAddUnit.add_liftRight_neg, AddCommute.addUnits_of_val, ofAddUnits_le_iff_le_addUnits, AddUnits.val_injective, AddUnits.val_neg_mulLeft, Nat.addUnits_eq_zero, IsAddUnit.addUnit_sub, AddUnits.neg_add, AddUnits.eq_neg_of_add_eq_zero_right, AddUnits.addCommute_coe_neg, AddSubmonoid.addUnits_iInf, AddSubmonoid.neg_mem_addUnits_iff, AddUnits.val_neg_mulRight, AddUnits.eq_neg_of_add_eq_zero_left, AddSubgroup.mem_ofAddUnits_iff_toAddUnits_mem, AddSemiconjBy.addUnits_neg_symm_left_iff, Set.addUnits_neg_mem_center, AddSemiconjBy.addUnits_neg_right_iff, AddUnits.instContinuousAdd, instCanLiftAddUnitsValIsAddUnit, AddUnits.neg_add_of_eq, AddUnits.val_zero, AddCommute.addUnits_val_iff, AddUnits.vaddAssocClass', Continuous.addUnits_map, AddUnits.val_sub_eq_sub_val, IsAddUnit.addUnit_neg, IsAddUnit.val_neg_apply, AddUnits.continuous_val, AddUnits.addLeft_symm, AddUnits.add_eq_zero_iff_neg_eq, AddUnits.instWeaklyLocallyCompactSpaceOfT1SpaceOfContinuousAdd, AddUnits.neg_eq_of_add_eq_zero_right, ContinuousMap.addUnitsLift_apply_neg_apply, AddUnits.neg_mul_right, AddUnits.add_neg_of_eq, AddSubmonoid.addUnits_mono, AddSubmonoid.addUnits_bot, AddUnits.val_vadd, AddUnits.neg_mulRight, AddSubmonoid.LocalizationMap.lift_apply, AddUnits.instFaithfulVAdd, AddMonoidHom.ker_toHomAddUnits, AddSubmonoid.val_addUnitsTypeEquivIsAddUnitAddSubmonoid_symm_apply, IsOfFinAddOrder.val_neg_addUnit, AddCommute.addUnits_neg_left_iff, AddUnits.val_nsmul_eq_nsmul_val, AddSubgroup.ofAddUnits_injective, AddSubgroup.ofAddUnits_sSup, AddUnits.neg_eq_val_neg, AddSubmonoid.coe_neg_val_add_coe_val, AddUnits.eq_zero, AddSubgroup.addUnit_of_mem_ofAddUnits_spec_mem, AddCommute.addUnits_zsmul_right, AddUnits.vaddCommClass_left, ContinuousMap.val_addUnitsLift_apply_apply, AddUnits.add_liftRight_neg, AddUnits.val_neg_inj, AddSubgroup.ofAddUnits_inf, AddSubmonoid.LocalizationMap.add_neg, AddUnits.addCommute_iff_add_neg_cancel_assoc, AddUnits.instDiscreteTopology, AddUnits.liftRight_neg_add, IsAddUnit.addUnit_add, AddSubgroup.ofAddUnits_mono, IsAddUnit.val_neg_add, AddSubmonoid.addUnits_inf, AddSubgroup.mem_ofAddUnits_iff_exists_isAddUnit, AddSubmonoid.LocalizationMap.neg_unique, AddUnits.coeHom_injective, AddUnits.isIsometricVAdd, AddUnits.map_bijective, AddUnits.addRight_symm, AddUnits.val_eq_zero, AddMonoidHom.coe_toHomAddUnits, AddUnits.add_neg_cancel_left, AddUnits.vaddAssocClass'_left, AddUnits.addCommute_iff_neg_add_cancel, AddUnits.add_neg_cancel_right, AddSubgroup.ofAddUnits_iSupβ, AddUnits.instT2Space, AddUnits.add_neg, AddUnits.isEmbedding_val, AddUnits.embedProduct_apply, AddSubgroup.mem_of_mem_val_ofAddUnits, AddUnits.neg_mulLeft, AddUnits.neg_add_eq_zero, AddUnits.coe_map_neg, Prod.instSubsingletonAddUnits, AddUnits.measurableVAdd, AddUnits.neg_mk, AddUnits.coe_map, AddUnits.map_injective, AddUnits.continuousVAdd, AddSemiconjBy.addUnits_zsmul_right, AddSubgroup.ofAddUnits_inf_addUnits, AddUnits.add_neg_eq_iff_eq_add, AddSubgroup.addUnit_mem_of_mem_ofAddUnits, ContinuousMap.val_addUnitsLift_symm_apply_apply, IsAddUnit.addUnit_neg_map, AddUnits.val_le_val, AddUnits.range_embedProduct, AddUnits.neg_add_cancel_right, AddUnits.val_add, AddSubmonoid.isOpen_addUnits, AddUnits.add_eq_zero_iff_eq_neg, AddEquiv.val_piAddUnits_symm_apply, IsAddUnit.coe_liftRight, AddUnits.neg_add_eq_neg_add_iff, AddCommute.addUnits_zsmul_left, AddUnits.instIsTopologicalAddGroupOfContinuousAdd, AddSubgroup.ofAddUnits_strictMono, AddUnits.isOpenMap_map, AddSubgroup.val_mem_ofAddUnits_iff_mem, AddUnits.eq_add_neg_iff_add_eq, AddUnits.map_id, AddUnits.neg_unique, AddSubmonoid.addUnits_left_inverse, Set.subset_addCenter_add_units, AddCommute.addUnits_neg_left, AddSubgroup.ofAddUnits_sup_addUnits, AddSubgroup.mem_addUnits_iff_val_mem, AddUnits.embedding_val_mk, AddSemiconjBy.addUnits_of_val, AddCommute.addUnits_neg_right_iff, AddUnits.vadd_neg, AddUnits.vaddCommClass_right, AddSubmonoid.IsUnit.Submonoid.coe_neg, AddEquiv.val_neg_piAddUnits_symm_apply, AddUnits.neg_add_eq_iff_eq_add, AddUnits.mk_addSemiconjBy, AddUnits.isOrderedAddMonoid, IsAddUnit.liftRight_neg_add, AddSubmonoid.mem_addUnits_iff, AddUnits.neg_add_cancel_left, AddUnits.neg_mul_eq_mul_neg, map_addUnits_neg, toAddUnits_symm_apply, AddUnits.coe_liftRight, AddUnits.instVAddAssocClass, AddUnits.val_lt_val, AddSubgroup.mem_ofAddUnits_iff, AddUnits.coe_opEquiv_symm, AddUnits.instLocallyCompactSpaceOfT1SpaceOfContinuousAdd, IsAddUnit.neg_vadd, AddUnits.instCompactSpaceOfT1SpaceOfContinuousAdd, AddSubmonoid.LocalizationMap.lift_mk', AddUnits.continuousConstVAdd, AddUnits.continuous_embedProduct, AddUnits.continuous_map, AddUnits.neg_nsmul_eq_nsmul_neg, AddUnits.val_neg_eq_neg_val, IsAddUnit.addUnit_zero, AddUnits.neg_mul_neg, AddUnits.addCommute_iff_add_neg_cancel, AddSubgroup.ofAddUnits_iSup, toAddUnits_val_apply, AddUnits.isClosedEmbedding_embedProduct, AddSubmonoid.addUnits_surjective, AddUnits.val_zsmul_eq_zsmul_val, AddUnits.neg_mul_left, AddUnits.instMeasurableConstVAdd, AddUnits.nsmul_ofNSMulEqZero, AddSubmonoid.addUnits_top, AddUnits.val_neg_ofNSMulEqZero, ContinuousMap.addUnitsLift_symm_apply_apply_neg', AddUnits.vadd_mk_apply, AddEquiv.val_piAddUnits_apply, AddUnits.topology_eq_inf, AddUnits.eq_neg_add_iff_add_eq, AddUnits.isEmbedding_embedProduct, AddUnits.isInducing_embedProduct, IsAddUnit.val_neg_addUnit', AddUnits.map_comp, AddSemiconjBy.addUnits_neg_symm_left, val_addUnitsCenterToCenterAddUnits_apply_coe, AddUnits.min_val, addUnitsCenterToCenterAddUnits_injective, AddUnits.addCommute_neg_coe, AddSubmonoid.LocalizationMap.add_neg_left, AddUnits.vaddCommClass', AddCommute.addUnits_neg_right, AddUnits.continuous_iff, AddSubgroup.exists_mem_ofAddUnits_val_eq, AddUnits.continuous_coe_neg, AddUnits.compare_val, AddUnits.max_val, AddUnits.add_neg_eq_zero
|
IsAddUnit π | MathDef | 58 mathmath: of_addIrreducible_add, IsAddUnit.of_add_eq_zero_right, AddCommute.isAddUnit_add_iff, IsAddUnit.add_iff, Finset.isAddUnit_iff, AddSubgroup.isAddUnit_of_mem_ofAddUnits, isAddUnit_unop, Prod.isAddUnit_iff, isAddUnit_iff_exists, AddSubmonoid.IsLocalizationMap.map_addUnits, addIrreducible_add_iff, isAddUnit_add_self_iff, AddGroup.isAddUnit, AddSubmonoid.isLocalizationMap_iff, Nat.isAddUnit_iff, AddUnits.isAddUnit_add_addUnits, AddOreLocalization.numerator_isAddUnit, instCanLiftAddUnitsValIsAddUnit, Matrix.isAddUnit_mul, AddSubmonoid.LocalizationMap.isAddUnit_comp, Pi.isAddUnit_iff, Set.isAddUnit_singleton, AddUnits.isAddUnit, IsOfFinAddOrder.isAddUnit, AddIrreducible.isAddUnit_or_isAddUnit, isAddUnit_nsmul_succ_iff, Set.isAddUnit_iff_singleton, AddUnits.isAddUnit_addUnits_add, IsAddUnit.of_nsmul_eq_zero, isAddUnit_iff_exists_neg, IsAddUnit.sum_iff, AddIrreducible.not_isAddUnit, isAddUnit_iff_exists_neg', IsAddUnit.of_add_eq_zero, isAddUnit_map_of_leftInverse, isAddUnit_op, isAddUnit_iff_eq_zero, Filter.isAddUnit_iff, addIrreducible_iff, IsAddUnit.isAddUnit_iff_addLeft_bijective, Filter.isAddUnit_pure, isAddUnit_iff_exists_and_exists, Matrix.isAddUnit_detp_smul_mul_adjp, Matrix.isAddUnit_iff, List.sum_isAddUnit_iff, IsAddUnit.sum_univ_iff, isAddUnit_nsmul_iff, isAddUnit_zero, Finset.isAddUnit_coe, LinearOrderedAddCommGroupWithTop.isAddUnit_iff, Finset.isAddUnit_singleton, Set.isAddUnit_iff, IsAddUnit.mem_addSubmonoid_iff, isAddUnit_of_subsingleton, AddSubmonoid.LocalizationMap.map_addUnits, AddEquiv.isAddUnit_map, Matrix.isAddUnit_detp_mul_detp, IsAddUnit.isAddUnit_iff_addRight_bijective
|
IsUnit π | MathDef | 445 mathmath: IsUnit.mul_iff, isUnit_cfc_iff, isUnit_of_mul_eq_one_right, Polynomial.isUnit_C_add_X_mul_iff, isUnit_cfc, MvPolynomial.dvd_monomial_one_iff_exists, ZMod.isUnit_iff_coprime, Rat.RingOfIntegers.isUnit_iff, IsNilpotent.isUnit_exp, quasispectrum_eq_spectrum_union, List.prod_isUnit_iff, IsLocalization.Away.algebraMap_isUnit_iff, Finset.isUnit_coe, StandardEtalePair.inv_aeval_X_g, Matrix.isUnit_of_right_inverse, isUnit_iff_exists, isRelPrime_self, Matrix.isUnit_det_zpow_iff, Polynomial.isPrimitive_iff_isUnit_of_C_dvd, AlgebraicGeometry.LocallyRingedSpace.notMem_prime_iff_unit_in_stalk, IsLocalization.Away.algebraMap_pow_isUnit, Polynomial.IsUnitTrinomial.coeff_isUnit, CharP.isUnit_ofNat_iff, not_isUnit_prime_of_dvd_card, Submonoid.IsLocalizationMap.map_units, Submonoid.isUnit_iff_and, Matrix.isUnit_det_of_invertible, IsArtinianRing.isUnit_of_mem_nonZeroDivisors, AlgebraicGeometry.Scheme.mem_basicOpen', analyticOnNhd_inverse, Units.nhds, Polynomial.not_isUnit_of_natDegree_pos, IsNilpotent.isUnit_sub_one, PowerSeries.eq_divided_by_X_pow_order_Iff_Unit, IsLocalRing.isUnit_or_isUnit_one_sub_self, CircleDeg1Lift.isUnit_iff_bijective, isUnit_iff_notMem_of_isAdicComplete_maximal, Module.Basis.isUnit_det, NormedSpace.isUnit_exp_of_mem_ball, IsLocalization.isUnit_comp, LinearMap.isUnit_iff_range_eq_top, prime_mul_iff, Matrix.exists_right_inverse_iff_isUnit, ZMod.val_unit', IsArtinianRing.isUnit_of_nonZeroDivisor_of_isIntegral', Filter.isUnit_iff_singleton, PowerSeries.isUnit_exp, Algebra.PreSubmersivePresentation.isUnit_jacobian_iff_aevalDifferential_bijective, Polynomial.IsPrimitive.isUnit_iff_isUnit_map_of_injective, Polynomial.not_isUnit_of_degree_pos_of_isReduced, isUnit_of_invertible, mem_nonunits_iff, MvPowerSeries.isUnit_iff_constantCoeff, ZMod.not_isUnit_of_mem_primeFactors, Polynomial.isUnit_map, WeierstrassCurve.IsElliptic.isUnit, PowerSeries.isUnit_divided_by_X_pow_order, FractionalIdeal.isUnit_num, CFC.continuousOn_log, IsArtinianRing.isUnit_iff_isRegular_of_mulOpposite, LinearMap.isUnit_iff_isUnit_det, spectrum.zero_notMem_iff, Ne.isUnit, PowerSeries.isUnit_iff_constantCoeff, IsUnit.smul_sub_iff_sub_inv_smul, Zsqrtd.norm_eq_one_iff, Int.ofNat_isUnit, Matrix.PosSemidef.posDef_iff_isUnit, associated_one_iff_isUnit, WeierstrassCurve.Projective.isUnit_dblU_of_Y_eq, AlgebraicGeometry.RingedSpace.mem_top_basicOpen, IsUnit.of_mul_eq_one, isUnit_map_of_leftInverse, spectrum.zero_mem_iff, Polynomial.isUnitTrinomial_iff, UniqueFactorizationMonoid.exists_prime_iff, Polynomial.isUnit_iff, LinearMap.isUnit_iff_ker_eq_bot, PowerSeries.IsWeierstrassDivision.isUnit_of_map_ne_zero, IsCoprime.isUnit_of_dvd', Localization.map_isUnit_of_le, Prod.isUnit_iff, IsIntegral.isUnit, MonomialOrder.isUnit_leadingCoeff, Matrix.isUnits_det_units, isQuasiregular_iff', WeierstrassCurve.Projective.isUnit_Y_of_Z_eq_zero, RingOfIntegers.isUnit_norm_of_isGalois, isUnit_pow_iff, ArchimedeanClass.FiniteElement.not_isUnit_iff_mk_pos, CStarAlgebra.isStrictlyPositive_iff_exists_isUnit_and_isSelfAdjoint_and_eq_mul_self, Polynomial.isUnit_iff', IsRightRegular.isUnit_of_finite, DivisorChain.element_of_chain_not_isUnit_of_index_ne_zero, Zsqrtd.norm_eq_one_iff', Matrix.PosDef.isUnit, PrimeSpectrum.basicOpen_le_basicOpen_iff_algebraMap_isUnit, Matrix.isUnit_fromBlocks_zeroββ, Irreducible.not_isUnit, isUnit_op, WeierstrassCurve.Projective.isUnit_addU_of_Y_ne, IsUnit.natCast_factorial_iff_of_charP, IsNilpotent.not_isUnit, Submonoid.isUnit_iff_of_ne_zero, MvPolynomial.isUnit_iff_totalDegree_of_isReduced, Matrix.isUnit_nonsing_inv_det_iff, ContinuousLinearMap.isUnit_of_forall_le_norm_inner_map, UniqueFactorizationMonoid.normalizedFactors_pos, ContinuousMap.isUnit_iff_forall_isUnit, MvPolynomial.isUnit_iff, spectrum.eventually_isUnit_resolvent, isUnit_gcd_one_right, Algebra.essFiniteType_cond_iff, CategoryTheory.isUnit_iff_isIso, smoothSheafCommRing.isUnit_stalk_iff, IsLocalization.isUnit_piRingHom_algebraMap_comp_piEvalRingHom, isLocalizedModule_iff, UniqueFactorizationMonoid.factors_pos, IsNilpotent.isUnit_add_one, Polynomial.not_isUnit_of_degree_pos, Matrix.isUnit_toLin'_iff, isSimpleModule_self_iff_isUnit, not_isUnit_zero, isUnit_iff_exists_inv, Matrix.isUnit_submatrix_equiv, IsNilpotent.isUnit_one_add, MulEquiv.isUnit_map, Submonoid.isUnit_iff, Set.isUnit_iff, Group.isUnit, isRelPrime_zero_right, Matrix.isUnit_det_J, Associated.isUnit_iff, Polynomial.Monic.isUnit_iff, isQuasiregular_iff_isUnit, Irreducible.isUnit_gcd_iff, IsPrimitiveRoot.geom_sum_isUnit, isLocalization_iff, Polynomial.not_isUnit_of_natDegree_pos_of_isReduced, IsUnit.sub_iff, IsPrimitiveRoot.isUnit, IsLocalization.algebraMap_isUnit_iff, Polynomial.isUnit_C, isUnit_of_mem_nonZeroDivisors, IsArtinianRing.isUnit_iff_mem_nonZeroDivisors, Ideal.span_singleton_eq_top, IsFractionRing.isUnit_map_of_injective, WfDvdMonoid.not_unit_iff_exists_factors_eq, Int.isUnit_iff_natAbs_eq, Polynomial.isUnit_resultant_iff_isCoprime, CStarAlgebra.isStrictlyPositive_iff_eq_mul_star_self, IsLocalization.Away.isUnit_of_dvd, isUnit_iff_ne_zero, ContinuousLinearMap.isUnit_iff_isUnit_toLinearMap, Filter.isUnit_iff, Module.End.isUnit_iff, IsUnit.mem_submonoid_iff, PowerSeries.isWeierstrassFactorizationAt_iff, IsUnit.neg_iff, Algebra.PreSubmersivePresentation.isUnit_jacobian_of_cotangentRestrict_bijective, isCoprime_zero_left, FiniteMultiplicity.not_unit, WeierstrassCurve.Projective.isUnit_dblZ_of_Y_ne, Matrix.UnitaryGroup.det_isUnit, Polynomial.IsUnitTrinomial.leadingCoeff_isUnit, CliffordAlgebra.isUnit_ΞΉ_iff, isUnit_smul_iff, QuadraticAlgebra.isUnit_iff_norm_isUnit, isUnit_iff_eq_one, IsUnit.of_mul_eq_one_right, Polynomial.isUnit_iff_coeff_isUnit_isNilpotent, Associates.mk_eq_one, Polynomial.IsUnitTrinomial.not_isUnit, MvPolynomial.isUnit_iff_eq_C_of_isReduced, Submonoid.LocalizationMap.isUnit_comp, PowerSeries.isUnit_weierstrassUnit, LinearEquiv.isUnit_det', PowerSeries.IsWeierstrassFactorizationAt.isUnit, Matrix.linearIndependent_cols_iff_isUnit, IsLocalization.localization_localization_map_units, spectrum.mem_resolventSet_iff, Polynomial.Separable.of_pow', Cardinal.isUnit_iff, Matrix.isUnit_toLin_iff, Matrix.posDef_iff_eq_conjTranspose_mul_self, Pi.isUnit_iff, PowerSeries.IsWeierstrassDivisorAt.isUnit_shift, IsArtinianRing.isUnit_iff_nonZeroDivisor_of_isIntegral, spectrum.isUnit_one_sub_smul_of_lt_inv_radius, PadicInt.isUnit_iff, HahnSeries.isUnit_iff, LaurentPolynomial.isUnit_T, Algebra.PreSubmersivePresentation.isUnit_jacobian_of_linearIndependent_of_span_eq_top, Associates.isUnit_iff_eq_bot, RingOfIntegers.isUnit_norm, extract_gcd, CategoryTheory.PreGaloisCategory.FibreFunctor.end_isUnit, Matrix.isUnit_fromBlocks_iff_of_invertibleββ, AddChar.val_isUnit, isUnit_unop, Matrix.PosSemidef.isUnit_sqrt_iff, isCoprime_self, Irreducible.isUnit_iff_not_associated_of_dvd, Prime.not_unit, isUnit_pow_succ_iff, isUnit_iff_not_dvd_char, Matrix.isUnit_iff_isUnit_det, isUnit_map_iff, IsLocalRing.isUnit_or_isUnit_of_add_one, IsUnit.natCast_of_isNilpotent_of_coprime, isUnit_zero_iff, Int.isUnit_iff_abs_eq, ZMod.coe_int_isUnit_iff_isCoprime, Polynomial.not_isUnit_X_add_C, IsArtinianRing.isUnit_iff_nonZeroDivisor_of_isIntegral', Matrix.isUnit_fromBlocks_zeroββ, ExteriorAlgebra.isUnit_algebraMap, ZMod.isUnit_prime_iff_not_dvd, IsStrictlyPositive.iff_of_unital, Units.isOpen, ArchimedeanClass.FiniteElement.isUnit_iff_mk_eq_zero, Matrix.isUnit_fromBlocks_iff_of_invertibleββ, IsUnit.natCast_factorial_of_algebra, Matrix.exists_left_inverse_iff_isUnit, WeierstrassCurve.Projective.isUnit_dblZ_of_Y_ne', IsArtinianRing.isUnit_iff_isLeftRegular, Set.isUnit_singleton, Polynomial.separable_C, TrivSqZeroExt.isUnit_inv_iff, FiniteDimensional.isUnit, PadicInt.isUnit_den, Valuation.Integers.isUnit_of_one', IsLocalRing.residue_ne_zero_iff_isUnit, isUnit_iff_mem_nonZeroDivisors_of_finite, squarefree_iff_emultiplicity_le_one, LinearEquiv.isUnit_det, Polynomial.isUnit_of_self_mul_dvd_separable, Nat.isUnit_iff, LinearMap.isUnit_toMatrix'_iff, IsCoprime.isUnit_of_dvd, WeierstrassCurve.isUnit_Ξ, CStarAlgebra.isUnit_of_le, gcd_isUnit_iff, isRegular_iff_isUnit_of_finite, Matrix.isUnit_comp_iff, Polynomial.Monic.irreducible_iff_degree_lt, isUnit_one, Matrix.isUnit_conjTranspose, EuclideanDomain.gcd_isUnit_iff, isUnit_gcd_of_eq_mul_gcd, WeierstrassCurve.Jacobian.isUnit_dblZ_of_Y_ne', DvdNotUnit.isUnit_of_irreducible_right, differentiableOn_inverse, IsDiscreteValuationRing.addVal_eq_zero_iff, spectrum.mem_iff, HomogeneousLocalization.isUnit_iff_isUnit_val, Polynomial.not_isUnit_X_sub_C, MvPolynomial.dvd_X_iff_exists, IsLocalization.surj_of_gcd_domain, CStarAlgebra.isStrictlyPositive_iff_isUnit_sqrt_and_eq_sqrt_mul_sqrt, IsLocalization.map_units_map_submonoid, Irreducible.isUnit_or_isUnit, Ideal.isUnit_of_sub_one_mem_jacobson_bot, isUnit_of_dvd_one, Polynomial.isUnit_primPart_C, LinearMap.isUnit_toMatrix_iff, Finset.isUnit_iff_singleton, Polynomial.Monic.C_dvd_iff_isUnit, Submonoid.isLocalizationMap_iff, IsUnit.mk0, isUnit_iff_not_dvd_char_of_ringChar_ne_zero, Matrix.vecMul_injective_iff_isUnit, Units.isUnit_mul_units, IsArtinianRing.isUnit_iff_mem_nonZeroDivisors_of_mulOpposite, TrivSqZeroExt.isUnit_inr_iff, Finset.isUnit_singleton, PadicInt.not_isUnit_iff, of_irreducible_mul, StandardEtalePair.HasMap.isUnit_derivative_f, IsGroupLikeElem.isUnit, Algebra.discr_isUnit_of_basis, Matrix.isUnit_charpolyRev_of_isNilpotent, TrivSqZeroExt.isUnit_or_isNilpotent_of_isMaximal_isNilpotent, ZMod.isUnit_prime_of_not_dvd, Matrix.isUnit_nonsing_inv_iff, dvd_pow_self_iff, CFC.isUnit_rpow_iff, isUnit_neg_one, IsLocalRing.isUnit_of_mem_nonunits_one_sub_self, Valuation.Integer.not_isUnit_iff_valuation_lt_one, IsNilpotent.isUnit_one_sub, isUnit_mul_self_iff, Ideal.isUnit_iff, Polynomial.isUnit_or_eq_zero_of_separable_expand, WeierstrassCurve.Jacobian.isUnit_Y_of_Z_eq_zero, DvdNotUnit.not_unit, Commute.isUnit_mul_iff, AffineBasis.isUnit_toMatrix_iff, gcd_isUnit_iff_isRelPrime, FractionalIdeal.mul_inv_cancel_iff_isUnit, CStarAlgebra.isStrictlyPositive_iff_eq_star_mul_self, IsLocalization.map_units, isUnit_gcd_one_left, AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen, spectrum.setOf_isUnit_inter_mul_comm, PowerSeries.heval_unit, IsLeftRegular.isUnit_of_finite, Polynomial.isUnit_iff_degree_eq_zero, isUnit_of_mul_eq_one, Irreducible.dvd_iff, AlgebraicGeometry.RingedSpace.isUnit_res_basicOpen, minpoly.not_isUnit, Associates.isUnit_iff_eq_one, Matrix.isUnit_det_of_left_inverse, Units.isUnit_units_mul, StarSubalgebra.coe_isUnit, UniqueFactorizationMonoid.primeFactors_eq_empty_iff, Ring.exists_not_isUnit_of_not_isField, IsArtinianRing.isUnit_of_mem_nonZeroDivisors_of_mulOpposite, AlgebraicGeometry.Scheme.mem_basicOpen_top, nonempty_invertible_iff_isUnit, irreducible_iff, Algebra.lmul_isUnit_iff, NumberField.isUnit_iff_norm, CStarAlgebra.isStrictlyPositive_TFAE, WittVector.isUnit_of_coeff_zero_ne_zero, Subgroup.isUnit_of_mem_ofUnits, OreLocalization.numerator_isUnit, Polynomial.Monic.isUnit_leadingCoeff_of_dvd, Valued.integer.isUnit_iff_norm_eq_one, Matrix.isUnit_of_left_inverse, Valuation.IsUniformizer.not_isUnit, Matrix.isUnit_exp, isUnit_iff_forall_dvd, spectrum.isUnit_of_zero_notMem, IsLocalRing.notMem_maximalIdeal, isQuasiregular_iff_isUnit', MulChar.trivial_apply, isCoprime_zero_right, IsLocalization.AtPrime.isUnit_mk'_iff, Matrix.mulVec_surjective_iff_isUnit, HahnSeries.isUnit_of_orderTop_pos, UniqueFactorizationMonoid.normalizedFactors_eq_zero_iff, isUnit_iff_exists_and_exists, IsRelPrime.isUnit_of_dvd, minpoly.IsIntegrallyClosed.isIntegral_iff_isUnit_leadingCoeff, WeierstrassCurve.isElliptic_iff, Module.End.isUnit_intrinsicStar_iff, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, Polynomial.not_isUnit_X_pow_sub_one, Valuation.Integers.isUnit_iff_valuation_eq_one, ZMod.isUnit_cast_of_dvd, IsUnit.prod_iff, IsUnit.isUnit_iff_mulRight_bijective, Associates.isUnit_mk, Filter.isUnit_pure, IsLocalizedModule.map_units, Algebra.SubmersivePresentation.jacobian_isUnit, instCanLiftUnitsValIsUnit, ZMod.eq_one_or_isUnit_sub_one, AlgebraicGeometry.Scheme.mem_basicOpen'', IsLocalization.AtPrime.isUnit_to_map_iff, CharP.isUnit_natCast_iff, Units.isUnit, IsStrictlyPositive.isUnit, Int.isUnit_iff, Zsqrtd.isUnit_iff_norm_isUnit, Finset.isUnit_iff, Polynomial.not_isUnit_X, Submonoid.LocalizationMap.map_units, isUnit_ringInverse, AlgebraicGeometry.LocallyRingedSpace.isUnit_res_toΞSpecMapBasicOpen, WeierstrassCurve.Jacobian.isUnit_dblZ_of_Y_ne, irreducible_mul_iff, ENNReal.isUnit_iff, ValuationSubring.valuation_eq_one_iff, Matrix.isUnit_transpose, IsUnit.prod_univ_iff, NormedSpace.isUnit_exp, TrivSqZeroExt.isUnit_inl_iff, TrivSqZeroExt.isUnit_iff_isUnit_fst, normalize_eq_one, CFC.isUnit_nnrpow_iff, isUnit_star, IsQuasiregular.isUnit_one_add, WeierstrassCurve.Jacobian.isUnit_X_of_Z_eq_zero, IsArtinianRing.isUnit_iff_isRightRegular, Algebra.essFiniteType_iff, Set.isUnit_iff_singleton, AffineBasis.isUnit_toMatrix, Matrix.isUnit_diagonal, TrivSqZeroExt.isUnit_or_isNilpotent, Polynomial.IsUnitTrinomial.trailingCoeff_isUnit, Polynomial.IsPrimitive.isUnit_iff_isUnit_map, IsNilpotent.isUnit_quotient_mk_iff, IsArtinianRing.isUnit_of_isIntegral_of_nonZeroDivisor, isUnit_of_subsingleton, ZMod.eq_unit_mul_divisor, DivisorChain.first_of_chain_isUnit, IsOfFinOrder.isUnit, Localization.awayLift_mk, isRelPrime_zero_left, Finset.isUnit_iff_singleton_aux, isUnit_of_associated_mul, ContinuousMap.isUnit_iff_forall_ne_zero, UniqueFactorizationMonoid.radical_eq_one_iff, IsUnit.isUnit_iff_mulLeft_bijective, UniqueFactorizationMonoid.factors_eq_zero, isUnit_iff_dvd_one, NormedField.nhdsWithin_isUnit_neBot, isUnit_two_iff_forall_even, AlgebraicGeometry.RingedSpace.mem_basicOpen, IsPrimePow.not_unit, IsUnit.natCast_factorial_of_isNilpotent, isOfFinOrder_iff_isUnit, WeierstrassCurve.Jacobian.isUnit_addZ_of_X_ne, SymplecticGroup.symplectic_det, WeierstrassCurve.Jacobian.isUnit_dblU_of_Y_eq, Module.Basis.is_basis_iff_det, EqualCharZero.PNat.isUnit_natCast, spectrum.isUnit_resolvent, IsFractionRing.isUnit_den_zero, Matrix.vecMul_surjective_iff_isUnit, Matrix.isUnit_det_of_right_inverse, IsLocalRing.isUnit_one_sub_self_of_mem_nonunits, IsUnit.of_pow_eq_one, WeierstrassCurve.Projective.isUnit_addZ_of_X_ne, isUnit_one_sub_of_norm_lt_one, Unitary.isUnit_coe, IsLocalization.Away.algebraMap_isUnit, IsArtinianRing.isUnit_iff_isRegular, CharP.isUnit_intCast_iff, ContinuousLinearMap.isUnit_iff_bijective, Matrix.mulVec_injective_iff_isUnit, Matrix.linearIndependent_rows_iff_isUnit, spectrum.not_isUnit_of_zero_mem, Matrix.isUnit_comp_symm_iff, IsFractionRing.isUnit_den_iff, Ideal.mem_jacobson_bot, spectrum.notMem_iff, WeierstrassCurve.Jacobian.isUnit_addU_of_Y_ne, AlgebraicGeometry.RingedSpace.mem_basicOpen', CFC.isUnit_sqrt_iff, AlgebraicGeometry.Scheme.mem_basicOpen, isUnit_iff_exists_inv'
|
commGroupOfIsUnit π | CompOp | β |
divp π | CompOp | 32 mathmath: Units.divp_sub, divp_eq_iff_mul_eq, Units.divp_add, divp_self, PowerSeries.constantCoeff_invUnitsSub, divp_assoc, divp_mul_cancel, Units.divp_add_divp, PowerSeries.coeff_invUnitsSub, mul_divp_cancel, divp_eq_div, divp_eq_one_iff_eq, Units.divp_sub_divp_same, divp_mul_eq_mul_divp, one_divp, divp_one, divp_divp_eq_divp_mul, divp_assoc', Units.divp_add_divp_same, Units.sub_divp, divp_mk0, divp_inv, inv_eq_one_divp', inv_eq_one_divp, Units.neg_divp, Units.divp_sub_divp, divp_mul_divp, divp_left_inj, divp_eq_divp_iff, val_div_eq_divp, eq_divp_iff_mul_eq, Units.add_divp
|
groupOfIsUnit π | CompOp | β |
invOfIsUnit π | CompOp | β |
Β«term_/β_Β» π | CompOp | β |
Β«term_Λ£Β» π | CompOp | β |