Units

📁 Source: Mathlib/Topology/ContinuousMap/Units.lean

Statistics

Metric	Count
Definitions addUnitsLift, unitsLift, unitsOfForallIsUnit, Units	4
Theorems addUnitsLift_apply_neg_apply, addUnitsLift_symm_apply_apply_neg', canLift, continuous_isUnit_unit, isUnit_iff_forall_isUnit, isUnit_iff_forall_ne_zero, spectrum_eq_preimage_range, spectrum_eq_range, unitsLift_apply_inv_apply, unitsLift_symm_apply_apply_inv', unitsOfForallIsUnit_apply, val_addUnitsLift_apply_apply, val_addUnitsLift_symm_apply_apply, val_unitsLift_apply_apply, val_unitsLift_symm_apply_apply	15
Total	19

ContinuousMap

Definitions

Name	Category	Theorems
addUnitsLift 📖	CompOp	4 math math: addUnitsLift_apply_neg_apply, val_addUnitsLift_apply_apply, val_addUnitsLift_symm_apply_apply, addUnitsLift_symm_apply_apply_neg'
unitsLift 📖	CompOp	4 math math: val_unitsLift_apply_apply, val_unitsLift_symm_apply_apply, unitsLift_apply_inv_apply, unitsLift_symm_apply_apply_inv'
unitsOfForallIsUnit 📖	CompOp	1 math math: unitsOfForallIsUnit_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addUnitsLift_apply_neg_apply 📖	mathematical	—	DFunLike.coe ContinuousMap instFunLike AddUnits.val instAddMonoidOfContinuousAdd AddUnits AddUnits.instNeg Equiv AddUnits.instTopologicalSpaceAddUnits EquivLike.toFunLike Equiv.instEquivLike addUnitsLift	—	—
addUnitsLift_symm_apply_apply_neg' 📖	mathematical	—	AddUnits.val AddUnits AddUnits.instNeg DFunLike.coe ContinuousMap AddUnits.instTopologicalSpaceAddUnits instFunLike Equiv instAddMonoidOfContinuousAdd EquivLike.toFunLike Equiv.instEquivLike Equiv.symm addUnitsLift	—	—
canLift 📖	mathematical	—	CanLift ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing Units.instTopologicalSpaceUnits Units.val DFunLike.coe instFunLike Continuous.comp Units.continuous_val continuous	—	Continuous.comp Units.continuous_val continuous ext
continuous_isUnit_unit 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing instFunLike	Continuous Units Units.instTopologicalSpaceUnits IsUnit.unit	—	continuous_induced_rng Continuous.prodMk continuous Continuous.comp MulOpposite.continuous_op continuous_iff_continuousAt NormedRing.inverse_continuousAt instHasSummableGeomSeriesOfCompleteSpace ContinuousAt.comp continuousAt
isUnit_iff_forall_isUnit 📖	mathematical	—	IsUnit ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing instMonoidOfContinuousMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalSeminormedRing.toIsTopologicalRing NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing DFunLike.coe instFunLike	—	IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing ext
isUnit_iff_forall_ne_zero 📖	mathematical	—	IsUnit ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedDivisionRing.toNormedRing instMonoidOfContinuousMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing	—	IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing NonUnitalSeminormedRing.toIsTopologicalRing isUnit_iff_forall_isUnit
spectrum_eq_preimage_range 📖	mathematical	—	spectrum ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedDivisionRing.toNormedRing Semifield.toCommSemiring Field.toSemifield NormedField.toField instRing NormedRing.toRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing algebra DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring IsTopologicalRing.toIsTopologicalSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Set.preimage DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap Set.range instFunLike	—	Set.ext IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalRing.toIsTopologicalSemiring Algebra.algebraMap_eq_smul_one
spectrum_eq_range 📖	mathematical	—	spectrum ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Semifield.toCommSemiring Field.toSemifield NormedField.toField instRing NormedRing.toRing NormedCommRing.toNormedRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing algebra DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.id IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Set.range DFunLike.coe instFunLike	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalRing.toIsTopologicalSemiring spectrum_eq_preimage_range Algebra.algebraMap_self Set.preimage_id
unitsLift_apply_inv_apply 📖	mathematical	—	DFunLike.coe ContinuousMap instFunLike Units.val instMonoidOfContinuousMul Units Units.instInv Equiv Units.instTopologicalSpaceUnits EquivLike.toFunLike Equiv.instEquivLike unitsLift	—	—
unitsLift_symm_apply_apply_inv' 📖	mathematical	—	Units.val Units Units.instInv DFunLike.coe ContinuousMap Units.instTopologicalSpaceUnits instFunLike Equiv instMonoidOfContinuousMul EquivLike.toFunLike Equiv.instEquivLike Equiv.symm unitsLift	—	—
unitsOfForallIsUnit_apply 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing DFunLike.coe ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing instFunLike	Units Units.instTopologicalSpaceUnits unitsOfForallIsUnit IsUnit.unit	—	—
val_addUnitsLift_apply_apply 📖	mathematical	—	DFunLike.coe ContinuousMap instFunLike AddUnits.val instAddMonoidOfContinuousAdd Equiv AddUnits AddUnits.instTopologicalSpaceAddUnits EquivLike.toFunLike Equiv.instEquivLike addUnitsLift	—	—
val_addUnitsLift_symm_apply_apply 📖	mathematical	—	AddUnits.val DFunLike.coe ContinuousMap AddUnits AddUnits.instTopologicalSpaceAddUnits instFunLike Equiv instAddMonoidOfContinuousAdd EquivLike.toFunLike Equiv.instEquivLike Equiv.symm addUnitsLift	—	—
val_unitsLift_apply_apply 📖	mathematical	—	DFunLike.coe ContinuousMap instFunLike Units.val instMonoidOfContinuousMul Equiv Units Units.instTopologicalSpaceUnits EquivLike.toFunLike Equiv.instEquivLike unitsLift	—	—
val_unitsLift_symm_apply_apply 📖	mathematical	—	Units.val DFunLike.coe ContinuousMap Units Units.instTopologicalSpaceUnits instFunLike Equiv instMonoidOfContinuousMul EquivLike.toFunLike Equiv.instEquivLike Equiv.symm unitsLift	—	—

(root)

Definitions

Name	Category	Theorems
Units 📖	CompData	1489 math math: Set.center_units_subset, CircleDeg1Lift.units_inv_apply_apply, units_inv_smul, IsUnit.unit_mul, Submonoid.units_iInf, WeierstrassCurve.j_of_char_two, spectrum.inv_mem_iff, Fin.sign_cycleIcc_of_eq, WithZero.logOrderIso_apply, Units.commute_iff_inv_mul_cancel, LaurentPolynomial.smeval_eq_sum, Valuation.IsRankOneDiscrete.generator_lt_one, IsLocalization.mul_add_inv_left, CochainComplex.HomComplex.δ_units_smul, unitsEquivNeZero_symm_apply, Units.mul_inv_of_eq, Matrix.GeneralLinearGroup.det_scalar, Commute.units_zpow_right, MulChar.equivToUnitHom_mul_apply, MonoidWithZeroHom.mem_valueGroup, ContinuousLinearEquiv.unitsEquiv_apply, AlternatingMap.domCoprod.summand_mk'', ZMod.isCyclic_units_iff_of_odd, Polynomial.ascPochhammer_smeval_neg_eq_descPochhammer, Matrix.det_apply, mem_rootsOfUnity, OrderMonoidIso.val_inv_unitsWithZero_symm_apply, WithZero.val_expOrderIso_apply, Subgroup.ofUnits_bot, ValuationSubring.coe_mem_principalUnitGroup_iff, Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_apply, ComplexShape.ε_succ, Units.le_mul_inv_of_mul_le, Units.min_val, WithZero.logEquiv_symm, Complex.linearEquiv_det_conjLIE, CircleDeg1Lift.translate_inv_apply, ClassGroup.mk0_integralRep, Units.commute_inv_coe, HNNExtension.toSubgroup_neg_one, ZMod.unitsMap_surjective, val_inv_unitsEquivProdSubtype_symm_apply, StandardEtalePair.inv_aeval_X_g, Matrix.GeneralLinearGroup.map_det, NumberField.Units.logEmbedding_fundSystem, modularCyclotomicCharacter.id, rootsOfUnityEquivOfPrimitiveRoots_apply_coe_inv_val, CochainComplex.HomComplex.Cochain.δ_single, MulChar.toUnitHom_eq, NumberField.Units.instNonemptySubtypeUnitsRingOfIntegersMemSubgroupTorsion, ModularForm.mul_slash, ComplexShape.χ_prev, CFC.inv_nonneg, autAdjoinRootXPowSubCEquiv_root, AffineSubspace.affineSpan_pair_parallel_iff_exists_unit_smul', PowerSeries.invOneSubPow_zero, MonoidWithZeroHom.snd_comp_inl, ClassGroup.mk_eq_mk_of_coe_ideal, spectrum.of_inv₀_mem, ZMod.rootsOfUnity_eq_top, Matrix.SpecialLinearGroup.coeToGL_det, Nat.card_units, NumberField.IsCMField.unitsComplexConj_torsion, normUnit_eq_one, IsUnit.unit_inv_map, WithZero.withZeroUnitsEquiv_symm_apply_coe, CategoryTheory.TwistShiftData.z_zero_zero, Orientation.linearEquiv_det_rotation, ComplexShape.EulerCharSigns.χ_next, NumberField.hermiteTheorem.minkowskiBound_lt_boundOfDiscBdd, IsUnit.unit_div, LinearEquiv.transvection.det_eq_one, ContinuousMultilinearMap.alternatization_apply_apply, AffineEquiv.coe_homothetyUnitsMulHom_eq_homothetyHom_coe, LinearEquiv.det_trans, ClassGroup.Quot_mk_eq_mk, AlternatingMap.map_perm, ZLattice.covolume_eq_det_inv, WeierstrassCurve.Projective.nonsingularLift_some, Unitary.toUnits_injective, spectrum.inv₀_mem_iff, Units.mul_inv_le_one_of_le, CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₁, Equiv.Perm.sign_of_cycleType, IsUnit.unit_inv, ZMod.units_pow_card_sub_one_eq_one, Matrix.det_permute, WithZero.coe_unitsWithZeroEquiv_eq_units_val, val_inv_unitarySubgroupUnitsEquiv_symm_apply_coe, Valuation.IsRankOneDiscrete.exists_generator_lt_one', PUnit.norm_unit_eq, Module.Ray.neg_units_smul, Units.compare_val, ComplexShape.eulerCharSignsDownNat_χ, Representation.asGroupHom_apply, SpecialLinearGroup.coe_zpow, IsCyclic.val_mulAutMulEquiv_apply, toMul_uzpow, SpecialLinearGroup.toLinearEquiv_symm_to_linearMap, Nat.factors_multiset_prod_of_irreducible, NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm_apply_fst, unitsNonZeroDivisorsEquiv_apply, spectrum.units_smul_resolvent_self, AddAut.mulRight_symm_apply, Units.inv_mul_le_of_le_mul, Matrix.trace_units_conj, DirichletCharacter.changeLevel_def, instSmallUnitsSkeletonModuleCat, Units.mul_inv_le_one, ofUnits_le_iff_le_units, NormedRing.inverse_add_norm_diff_nth_order, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₃, NumberField.mixedEmbedding.norm_unit_smul, Set.unit_eq, ZMod.isCyclic_units_two_mul_iff_of_odd, WeierstrassCurve.variableChange_a₁, Units.smul_coe, SpecialLinearGroup.mem_center_iff_spec, CommGroup.monoidHom_mulEquiv_of_hasEnoughRootsOfUnity, uzpow_zero, Module.Basis.repr_isUnitSMul, cyclotomicCharacter.toZModPow, UpperHalfPlane.im_smul_eq_div_normSq, OrderMonoidIso.val_unitsCongr_symm_apply, Commute.units_inv_right_iff, Submonoid.inv_mem_units_iff, PowerSeries.Unit_of_divided_by_X_pow_order_zero, Matrix.detp_neg_one_one, WeierstrassCurve.variableChange_Δ', ConjAct.unitsSMulCommClass', pinGroup.val_inv_toUnits_apply, Valuation.IsRankOneDiscrete.generator_mem_valueGroup, ENNReal.mulRightOrderIso_symm_apply, ComplexShape.associative_ε₂_ε₁, Equiv.Perm.signAux_swap, LinearOrderedCommGroupWithZero.inl_mul_inr_eq_coe_toLex, Matrix.charpoly_units_conj', HomologicalComplex.mapBifunctor₂₃.d₂_eq, Set.unitEquivUnitsInteger_symm_apply_coe, Equiv.Perm.val_equivUnitsEnd_apply, CategoryTheory.Pretriangulated.Triangle.shiftFunctor_obj, val_unitarySubgroupUnitsEquiv_symm_apply_coe, SpecialLinearGroup.mem_center_iff, ZMod.unitsMap_self, HNNExtension.NormalWord.ReducedWord.chain, Valued.toUniformSpace_eq, Valuation.instNontrivialSubtypeUnitsMemSubmonoidValueMonoidOfIsNontrivial, ker_zpowGroupHom_eq_rootsOfUnity, Module.Ray.units_smul_of_neg, uzpow_natCast, IsPrimitiveRoot.val_toRootsOfUnity_coe, UpperHalfPlane.moebius_im, ModularForm.prod_slash, CommRing.Pic.mul_eq_tensor, Complex.isQuotientCoveringMap_npow, ContinuousMap.val_unitsLift_apply_apply, Subgroup.mem_ofUnits_iff_exists_isUnit, HomologicalComplex₂.totalAux.d₂_eq, Equiv.Perm.sign_subtypePerm, rootsOfUnity.integer_power_of_ringEquiv, mem_principal_ideals_iff, HomologicalComplex₂.D₂_totalShift₁XIso_hom_assoc, Submonoid.units_bot, subgroup_units_cyclic, IsUnit.mul_val_inv, Units.inv_eq_self_iff, HNNExtension.NormalWord.t_smul_eq_unitsSMul, LinearEquiv.conjAlgEquiv_ext_iff', Units.coe_liftRight, HomologicalComplex₂.D₂_totalShift₂XIso_hom_assoc, ComplexShape.ε_add, IsLocalizedModule.iso_apply_mk, SpecialLinearGroup.coe_one, Subgroup.ofUnits_strictMono, CochainComplex.HomComplex.Cocycle.coe_units_smul, normUnit_mul_normUnit, CategoryTheory.CatCenter.smul_iso_inv_eq', rootsOfUnity.isCyclic, Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_symm_apply_coe_coe, CochainComplex.HomComplex.Cochain.units_smul_comp, MonoidWithZeroHom.coe_one, LaurentPolynomial.smeval_T_pow, autAdjoinRootXPowSubCEquiv_symm_smul, ConjAct.unitsSMulCommClass, IsCyclic.monoidHom_mulEquiv_rootsOfUnity, Nat.two_le_radical_iff, ModularForm.prod_slash_sum_weights, Int.negOnePow_eq_neg_one_iff, MonoidHom.toHomPerm_apply_symm_apply, Complex.instPathConnectedSpaceUnits, HomologicalComplex.mapBifunctor₂₃.d₃_eq, IsPrimitiveRoot.pow_sub_one_eq_geom_sum_mul_geom_sum_inv_mul_pow_sub_one, WeierstrassCurve.Projective.Point.zero_point, ModularGroup.coe_apply_complex, Units.inv_eq_of_mul_eq_one_right, Submodule.ker_unitsToPic, Equiv.Perm.sign_trans_trans_symm, WeierstrassCurve.j_of_char_three, WithZero.coe_expEquiv_apply, Matrix.GeneralLinearGroup.center_eq_range_scalar, ZMod.isCyclic_units_one, SpecialLinearGroup.mem_range_toGeneralLinearGroup_iff, Units.coe_neg_one, MonoidWithZeroHom.fst_mono, quasispectrum.mem_iff_of_isUnit, Equiv.Perm.viaFintypeEmbedding_sign, PreQuasiregular.add_inv_add_mul_eq_zero, uzpow_coe_nat, CochainComplex.ι_mapBifunctorShift₂Iso_hom_f_assoc, MulEquiv.val_piUnits_symm_apply, mem_rootsOfUnity_prime_pow_mul_iff', val_unitsCentralizerEquiv_apply_coe, Equiv.Perm.sign_symm, MonoidHom.ker_toHomUnits, SpecialLinearGroup.centerCongr_toLin_equiv_trans_centerEquivRootsOfUnity_eq, Complex.mem_rootsOfUnity, Ideal.rootsOfUnityMapQuot_injective, Int.normUnit_eq, Valuation.ltAddSubgroup_monotone, NumberField.Units.coe_mul, ZMod.isCyclic_units_iff, Units.one_le_inv_of_le, Units.index_posSubgroup, mem_rootsOfUnity_iff_mem_nthRoots, Polynomial.monic_of_isUnit_leadingCoeff_inv_smul, CochainComplex.HomComplex.δ_v, HomologicalComplex₂.ιTotal_totalFlipIso_f_inv_assoc, Units.smulCommClass_left, LinearEquiv.det_baseChange, Polynomial.natDegree_of_dvd_cyclotomic_of_irreducible, Matrix.det_units_conj', rootsOfUnity.coe_injective, Units.isOfFinOrder_val, Fin.sign_cycleRange, Equiv.Perm.sign_eq_prod_prod_Ioi, PreQuasiregular.inv_add_add_mul_eq_zero, WeierstrassCurve.Projective.addMap_of_Z_eq_zero_left, CategoryTheory.Linear.units_smul_comp, spinGroup.units_mem_lipschitzGroup, WeierstrassCurve.Jacobian.Point.fromAffine_some, RootPairing.Equiv.toEndUnit_inv, Equiv.Perm.prod_Ioi_comp_eq_sign_mul_prod, LaurentPolynomial.eval₂_C_mul_T, Matrix.coe_units_inv, ValuativeRel.subsingleton_units_valueGroupWithZero_of_trivialRel, Polynomial.normUnit_content, disjoint_rootsOfUnity_of_coprime, Units.instStarModule, LocalizedModule.lift'_mk, Valuation.unit_map_eq, Units.val_inv_eq_inv_val, orderOf_units, alternatingGroup.normalClosure_swap_mul_swap_five, Units.inv_le_one, CategoryTheory.CatCenter.smul_iso_inv_eq'_assoc, NumberField.mixedEmbedding.fundamentalCone.integerSetQuotEquivAssociates_apply, CochainComplex.HomComplex.Cochain.rightUnshift_units_smul, ComplexShape.ε₁_ε₂, ZMod.AddAutEquivUnits_symm_apply, uzpow_one, Asymptotics.isBigOWith_self_const_mul', Valuation.IsUniformizer.zpowers_eq_valueGroup, HNNExtension.toSubgroupEquiv_neg_one, unitsEquivProdSubtype_apply_coe, Units.smul_mk0, val_unitsCenterToCenterUnits_apply_coe, ContinuousLinearEquiv.unitsEquivAut_apply, NormalizationMonoid.normUnit_coe_units, Units.val_inv_inj, WithZero.expOrderIso_symm_apply, Units.mul_liftRight_inv, PowerSeries.IsWeierstrassFactorization.isWeierstrassDivision, CommGroup.card_monoidHom_of_hasEnoughRootsOfUnity, Equiv.Perm.sign_of_cycleType_eq_replicate, Units.coe_map, Units.map_mk, Units.isIsometricSMul, pinGroup.val_toUnits_apply, MulChar.mulEquiv_units, IsUnit.inv_smul, Units.inv_eq_val_inv, Units.instCompactSpaceOfT1SpaceOfContinuousMul, Units.continuous_val, PowerSeries.normUnit_X, GradedTensorProduct.tmul_coe_mul_coe_tmul, Subgroup.mem_ofUnits_iff, uzpow_mul, Nat.radical_pos, ZMod.pow_totient, ComplexShape.TensorSigns.ε'_succ, ComplexShape.ε_down_ℕ, Subgroup.ofUnits_le_ofUnits_iff, spinGroup.val_inv_toUnits_apply, Units.mul_inv_mem_unitary, Subsingleton.units_of_isUnit, rootsOfUnity_one, OrderMonoidIso.val_unitsCongr_apply, Matrix.inv_smul', hasFDerivAt_ringInverse, HasEnoughRootsOfUnity.natCard_rootsOfUnity, TotalComplexShapeSymmetry.σ_ε₁, MonoidWithZeroHom.mem_valueMonoid, Units.pow_ofPowEqOne, WeierstrassCurve.toCharNeTwoNF_u, Equiv.Perm.decomposeFin.symm_sign, IsPrimitiveRoot.autToPow_eq_modularCyclotomicCharacter, Units.instIsTopologicalGroupOfContinuousMul, NumberField.mixedEmbedding.fundamentalCone.integerSetEquiv_apply_fst, HNNExtension.toSubgroup_one, CliffordAlgebra.map_mul_map_of_isOrtho_of_mem_evenOdd, ZMod.not_isCyclic_units_of_mul_coprime, Units.map_bijective, Fintype.card_units, CategoryTheory.Aut.toEnd_apply, AffineEquiv.linear_equivUnitsAffineMap_symm_apply, Units.mul_inv_eq_iff_eq_mul, WeierstrassCurve.Jacobian.negMap_of_Z_ne_zero, Nat.card_units_zmod_lt_sub_one, rootsOfUnity.val_mkOfPowEq_coe, Ring.choose_neg, HomologicalComplex₂.ι_totalShift₂Iso_inv_f_assoc, CochainComplex.HomComplex.Cochain.leftShift_comp, CFC.rpow_neg, NumberField.Units.map_complexEmbedding_torsion, CircleDeg1Lift.coe_toOrderIso_symm, CircleDeg1Lift.translate_iterate, unitarySubgroupUnitsEquiv_apply_coe, NumberField.Units.span_basisOfIsMaxRank, Int.negOnePow_two_mul, NormalizationMonoid.normUnit_zero, Matrix.GeneralLinearGroup.continuous_det, Commute.units_of_val, MulEquiv.restrictRootsOfUnity_symm, Units.coe_prod, WeierstrassCurve.Jacobian.nonsingularLift_iff, IsPrimitiveRoot.coe_autToPow_apply, WeierstrassCurve.variableChange_b₈, NumberField.Units.logEmbeddingQuot_apply, CategoryTheory.Preadditive.smul_iso_hom, instIsCyclicUnitsWithZero, Submonoid.coe_inv_val_mul_coe_val, val_toUnits_apply, Units.conj_pow', NumberField.Units.basisOfIsMaxRank_apply, Units.instIsScalarTower, AlternatingMap.map_congr_perm, PowerSeries.coeff_invOfUnit, Subgroup.exists_mem_ofUnits_val_eq, Units.map_neg, Units.map_injective, CategoryTheory.TwistShiftData.assoc, unitary.toUnits_comp_map, Set.units_inv_mem_center, CircleDeg1Lift.coe_toOrderIso_inv, Units.instDiscreteTopology, OrderMonoidIso.val_inv_unitsCongr_symm_apply, Units.orderEmbeddingVal_apply, unitSphereToUnits_apply_coe, Subgroup.mem_of_mem_val_ofUnits, OrderMonoidIso.withZeroUnits_symm_apply, ZMod.dft_comp_unitMul, Equiv.Perm.sign_prodExtendRight, Units.inv_mul, WeierstrassCurve.VariableChange.mul_def, coe_toPrincipalIdeal, NumberField.mixedEmbedding.fundamentalCone.integerSetTorsionSMul_smul_coe, MonoidWithZeroHom.inl_strictMono, units_smul_eq_self_iff, WithZero.expEquiv_symm, spectrum.smul_mem_smul_iff, instFiniteMonoidHomUnits, Set.coe_unit, spinGroup.units_involute_act_eq_conjAct, MvPowerSeries.constantCoeff_invOfUnit, Valuation.subgroups_basis, DirichletCharacter.mulEquiv_units, OrderMonoidIso.withZeroUnits_apply, SpecialLinearGroup.coe_inv, CommRing.Pic.inv_eq_dual, CochainComplex.HomComplex.Cochain.leftShift_rightShift_eq_negOnePow_rightShift_leftShift, units_smul_eq_neg_iff, Module.End.algebraMap_isUnit_inv_apply_eq_iff', NumberField.Units.instFiniteIntAdditiveUnitsRingOfIntegers, FiniteField.forall_pow_eq_one_iff, spectrum.resolvent_eq, card_units_lt, Equiv.Perm.sign_abs, WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_neg_mul, IsDedekindDomain.selmerGroup.monotone, Fin.sign_cycleIcc_of_ge, Valuation.mem_unitGroup_iff, HomologicalComplex₂.d₁_eq, Submonoid.coe_val_mul_coe_inv_val, HasEnoughRootsOfUnity.rootsOfUnity_isCyclic, CochainComplex.HomComplex.Cochain.leftShift_rightShift, val_inv_unitsNonZeroDivisorsEquiv_symm_apply_coe, spinGroup.conjAct_smul_ι_mem_range_ι, MulChar.equivToUnitHom_symm_coe, Units.instIsManifoldModelWithCornersSelf, fderiv_inverse, Nat.units_eq_one, Algebra.SubmersivePresentation.jacobianRelations_spec, Units.coe_map_inv, Matrix.detp_one_one, CircleDeg1Lift.units_apply_inv_apply, MulChar.pow_card_eq_one, Units.inv_mul_le_one_of_le, OrderMonoidIso.val_unitsWithZero_symm_apply, DihedralGroup.oddCommuteEquiv_symm_apply, MonoidWithZeroHom.valueMonoid_eq_valueGroup, Units.coe_star, ComplexShape.Associative.ε₂_ε₁, Units.coe_smul, CommRing.Pic.mk_eq_iff, ComplexShape.ε₁_def, Int.units_pow_two, Units.divp_add_divp, Units.mul_inv_eq_mul_inv_iff, CategoryTheory.Preadditive.smul_iso_inv, Module.Basis.det_unitsSMul, Units.val_set_image_rootsOfUnity_one, spinGroup.involute_act_ι_mem_range_ι, denselyOrdered_units_iff, IsStarNormal.val_inv, OrderIso.withZeroUnits_symm_apply, CommMonCat.val_units_map_hom_apply, Units.instContinuousMul, Int.units_inv_eq_self, LaurentPolynomial.eval₂_T, Units.instLocallyCompactSpaceOfT1SpaceOfContinuousMul, MultilinearMap.domCoprod_alternization_coe, unitSphereToUnits_injective, FiniteField.sum_subgroup_units_eq_zero, Matrix.det_eq_detp_sub_detp, Submonoid.val_inv_unitsTypeEquivIsUnitSubmonoid_symm_apply, WeierstrassCurve.Projective.smul_eq, Nonneg.val_unitsEquivPos_symm_apply_coe, NumberField.Units.complexEmbedding_injective, ValuationSubring.principalUnitGroup_le_principalUnitGroup, Polynomial.roots_C_mul_X_sub_C_of_IsUnit, CommRing.Pic.mk_eq_self, spinGroup.conjAct_smul_range_ι, SpecialLinearGroup.congr_linearEquiv_coe_apply, WeierstrassCurve.variableChange_b₂, IsPrimitiveRoot.autToPow_injective, MonoidWithZeroHom.valueGroup_eq_range, Equiv.Perm.sign_trans, AffineEquiv.coe_homothetyUnitsMulHom_apply_symm, DirichletCharacter.Even.toUnitHom_eval_neg_one, ArithmeticFunction.pow_carmichael, Valued.hasBasis_nhds_zero, Int.negOnePow_add, Valuation.IsRankOneDiscrete.instIsCyclicSubtypeUnitsMemSubgroupValueGroup, ZMod.card_units, ZMod.card_units_eq_totient, WithZero.instNontrivialUnits, Units.smul_isUnit, Equiv.Perm.signAux_one, CommMonCat.val_inv_units_map_hom_apply, SpecialLinearGroup.det_eq_one, PowerSeries.constantCoeff_invOfUnit, WeierstrassCurve.Affine.nonsingular_iff_variableChange, Algebra.SubmersivePresentation.map_invJacobianOfHasCoeffs, WeierstrassCurve.variableChange_b₆, UnitsInt.univ, modularCyclotomicCharacter.toFun_spec, WeierstrassCurve.Jacobian.negMap_of_Z_eq_zero, ZMod.inv_coe_unit, isQuotientCoveringMap_npow, Nonneg.val_unitsHomeomorphPos_symm_apply_coe, DirichletCharacter.toUnitHom_eq_char', IsCyclic.val_inv_mulAutMulEquiv_apply, Equiv.Perm.sign_sumCongr, MulChar.apply_mem_rootsOfUnity_of_pow_eq_one, NumberField.Units.fundSystem_mk, WeierstrassCurve.Affine.equation_iff_variableChange, DirichletCharacter.changeLevel_toUnitHom, Equiv.Perm.sign_eq_prod_prod_Iio, LinearMap.CompatibleSMul.units, HNNExtension.NormalWord.unitsSMul_cancels_iff, WithZero.withZeroUnitsEquiv_symm_strictMono, instNontrivialUnitsOfDenselyOrdered, ContinuousLinearEquiv.symm_smul_apply, ZMod.unitsMap_comp, MulEquiv.restrictRootsOfUnity_coe_apply, ZMod.instSubsingletonUnits, WeierstrassCurve.VariableChange.inv_def, FractionalIdeal.canonicalEquiv_mk0, NumberField.IsCMField.indexRealUnits_mul_eq, NumberField.Units.dirichletUnitTheorem.map_logEmbedding_sup_torsion, CommRing.Pic.mapAlgebra_apply, HNNExtension.NormalWord.ReducedWord.empty_toList, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₁, Matrix.det_permutation, IsPrimitiveRoot.card_rootsOfUnity, CommRing.Pic.ext_iff, ContinuousMap.unitsOfForallIsUnit_apply, HomologicalComplex.units_smul_f_apply, HasEnoughRootsOfUnity.cyc, IsOpenUnits.isOpenEmbedding_unitsVal, CochainComplex.HomComplex.Cochain.leftUnshift_v, Units.val_le_val, NumberField.mixedEmbedding.unit_smul_eq_iff_mul_eq, MulChar.sum_one_eq_card_units, NumberField.InfinitePlace.ComplexEmbedding.conjugate_sign, ComplexShape.associative_ε₂_eq_mul, NumberField.mixedEmbedding.fundamentalCone.unit_smul_mem_iff_mem_torsion, Submodule.linearEquiv_det_reflection, WithZero.unitsWithZeroEquiv_symm_apply, ValuationSubring.coe_unitGroupMulEquiv_apply, ContinuousMap.val_unitsLift_symm_apply_apply, NumberField.mixedEmbedding.fundamentalCone.integerSetTorsionSMul_stabilizer, Submonoid.LocalizationMap.inv_unique, NumberField.Units.rank_modTorsion, Units.mul_inv_cancel_right, CommRing.Pic.instFreeAsModuleOfNat, ValuationSubring.unitGroup_injective, MonoidHom.coe_toHomUnits, Units.inv_eq_of_mul_eq_one_left, ConjAct.units_smul_def, AffineEquiv.val_equivUnitsAffineMap_apply, Units.val_set_image_rootsOfUnity, Submodule.IsLattice.smul, spectrum.units_conjugate, PrincipalIdeals.normal, PowerSeries.coeff_invUnitsSub, CochainComplex.HomComplex.Cochain.rightShift_leftShift, Units.instLieGroupModelWithCornersSelf, WeierstrassCurve.Jacobian.nonsingularLift_some, MulEquiv.val_inv_piUnits_apply, Subgroup.HasDetOne.det_eq, NumberField.Units.dirichletUnitTheorem.sum_logEmbedding_component, IsPrimitiveRoot.coe_units_iff, CategoryTheory.CatCenter.smul_iso_hom_eq'_assoc, Units.inv_mk, IsLocalization.lift_mk', IsUnit.coe_liftRight, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom, ValuationSubring.mem_unitGroup_iff, Module.Ray.units_smul_of_pos, HNNExtension.NormalWord.unitsSMulGroup_snd, Submonoid.unitsTypeEquivIsUnitSubmonoid_apply_coe, Orientation.map_eq_det_inv_smul, Units.mul_inv_le_iff, MonoidWithZeroHom.fst_comp_inl, LucasLehmer.X.card_units_lt, HNNExtension.NormalWord.unitsSMul_one_group_smul, unitary.toUnits_injective, Units.val_zpow_eq_zpow_val, HomologicalComplex₂.totalAux.d₂_eq', Units.mapEquiv_symm, CStarAlgebra.inv_le_inv_iff, Units.one_le_inv, HomologicalComplex₂.totalAux.d₁_eq, Units.smul_mk_apply, HomologicalComplex₂.D₁_totalShift₂XIso_hom_assoc, NumberField.IsCMField.unitsMulComplexConjInv_apply_torsion, NumberField.mixedEmbedding.fundamentalCone.exists_unitSMul_mem_integerSet, Units.inv_unique, LinearEquiv.det_symm, Nonneg.val_inv_unitsHomeomorphPos_symm_apply_coe, HomologicalComplex.mapBifunctor.d₂_eq, Submonoid.units_isCompact, IsCyclic.monoidHom_equiv_self, IsLocalizedModule.fromLocalizedModule_mk, HomologicalComplex.ι_mapBifunctorFlipIso_inv_assoc, Units.unitary_eq, SpecialLinearGroup.centerEquivRootsOfUnity_symm_apply, Units.mem_posSubgroup, pinGroup.conjAct_smul_ι_mem_range_ι, Submonoid.units_top, Unitization.val_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, Equiv.Perm.sign_bij, LinearOrderedCommGroupWithZero.inl_eq_coe_inlₗ, NumberField.mixedEmbedding.fundamentalCone.quotIntNorm_apply, OrderMonoidIso.unitsWithZero_apply, NumberField.Units.mem_torsion, Submonoid.isOpen_units, WithZero.val_inv_expOrderIso_apply, Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe, Int.units_pow_eq_pow_mod_two, map_rootsOfUnity_eq_pow_self, ComplexShape.ε₂_ε₁, val_unitsNonZeroDivisorsEquiv_symm_apply_coe, Submonoid.units_sInf, WeierstrassCurve.variableChange_def, Units.val_eq_neg_one, Fin.sign_cycleIcc_of_le, Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator, SpecialLinearGroup.det_coe, WeierstrassCurve.Projective.addMap_eq, spectrum.inv₀_mem_inv_iff, Units.commute_iff_inv_mul_cancel_assoc, ZMod.AddAutEquivUnits_apply, MonoidHom.toHomUnits_mul, Subgroup.val_centerUnitsEquivUnitsCenter_symm_apply_coe, Matrix.inv_adjugate, Units.mulLeft_symm, NumberField.Units.regOfFamily_div_regulator, NumberField.mixedEmbedding.fundamentalCone.exists_unit_smul_mem, IsUnit.mul_liftRight_inv, Commute.units_inv_left_iff, Units.mul_inv, Units.inv_pos, WeierstrassCurve.Jacobian.addMap_of_Z_ne_zero, CategoryTheory.Linear.comp_units_smul, Units.val_inv_ofPowEqOne, Units.symm_mapContinuousMulEquiv, Int.negOnePow_one, Equiv.Perm.mem_alternatingGroup, Equiv.Perm.ofSign_disjoint, Matrix.det_reindex, ContinuousMap.unitsLift_apply_inv_apply, groupCohomology.norm_ofAlgebraAutOnUnits_eq, Equiv.Perm.sign_of_pow_two_eq_one, WeierstrassCurve.variableChange_a₂, rootsOfUnity_eq_ker, NumberField.Units.coe_neg_one, Valuation.IsRankOneDiscrete.generator_zpowers_eq_range, WeierstrassCurve.variableChange_a₃, Units.inv_mul_le_iff, unitsCenterToCenterUnits_injective, CStarAlgebra.inv_le_iff, HomologicalComplex₂.D₁_totalShift₁XIso_hom_assoc, Projectivization.mk_eq_mk_iff, Int.units_div_eq_mul, ENNReal.mulLeftOrderIso_symm_apply, Units.max_val, CStarAlgebra.le_inv_iff, NumberField.mixedEmbedding.logMap_eq_logEmbedding, ZMod.euler_criterion_units, instIsCyclicUnitsOfFinite, OrderMonoidIso.val_inv_unitsCongr_apply, Equiv.Perm.sign_refl, Units.val_div_eq_div_val, Units.isEmbedding_embedProduct, AddChar.val_mem_rootsOfUnity, NumberField.IsCMField.closure_realFundSystem_sup_torsion, MonoidWithZeroHom.inl_mul_inr_eq_mk_of_unit, ContinuousLinearEquiv.symm_smul, CochainComplex.HomComplex.δ_comp, bijective_rootsOfUnityAddChar, NumberField.Units.instIsCyclicSubtypeUnitsRingOfIntegersMemSubgroupTorsion, WeierstrassCurve.Jacobian.addMap_of_Z_eq_zero_right, WeierstrassCurve.variableChange_c₆, Units.isOpenMap_map, Submonoid.units_surjective, Submonoid.LocalizationMap.lift_mk', Units.inv_pow_eq_pow_inv, Set.val_unitEquivUnitsInteger_apply_coe, Units.commute_coe_inv, unitary.val_toUnits_apply, IsCyclotomicExtension.Rat.galEquivZMod_apply_of_pow_eq, NormedRing.inverse_add, Submonoid.units_left_inverse, Valuation.ltSubmodule_monotone, Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_apply, IsDedekindDomain.HeightOneSpectrum.valuation_of_unit_eq, Int.negOnePow_odd, Units.liftRight_inv_mul, Units.coe_unop_opEquiv, Units.sq_eq_sq_iff_eq_or_eq_neg, ComplexShape.σ_ε₁, Units.measurableSMul, SpecialLinearGroup.coe_mul, Units.instMeasurableConstSMul, Subgroup.mem_ofUnits_iff_toUnits_mem, rootsOfUnity.coe_mkOfPowEq, ValuationSubring.unitGroup_strictMono, Units.toAut_hom, ContinuousLinearEquiv.trans_smul, CircleDeg1Lift.translate_apply, Subgroup.ofUnits_inf, Nonneg.unitsHomeomorphPos_apply_coe, cfcUnits_pow, NormedRing.inverse_one_sub, NumberField.Units.closure_fundSystem_sup_torsion_eq_top, Int.negOnePow_def, Submodule.unitsToPic_apply, Units.map_id, Units.mul_eq_one_iff_eq_inv, ComplexShape.associative_ε₁_eq_mul, cfc_comp_zpow, Units.smulCommClass_right, Submodule.range_unitsToPic, Ring.choose_neg', AbsoluteValue.map_units_int_smul, AffineEquiv.equivUnitsAffineMap_symm_apply_apply, ofUnits_units_gc, LinearIsometryEquiv.toLinearEquiv_smul, HomologicalComplex₂.ιTotal_totalFlipIso_f_hom_assoc, Units.instWeaklyLocallyCompactSpaceOfT1SpaceOfContinuousMul, LinearEquiv.symm_smul, Units.val_inv_cfcRpow, NormedSpace.exp_units_conj', WeierstrassCurve.coe_inv_variableChange_Δ', Unitary.toAlgEquiv_conjStarAlgAut, Equiv.Perm.sign_mul, Nat.factors_eq, LinearEquiv.det_conj, CategoryTheory.TwistShiftData.z_zero_left, val_unitsEquivProdSubtype_symm_apply, pinGroup.units_mem_iff, WeierstrassCurve.inv_variableChange_Δ', WeierstrassCurve.Projective.Point.fromAffine_some, CFC.rpow_neg_one_eq_inv, Matrix.nonsing_inv_apply, Nonneg.unitsEquivPos_apply_coe, CochainComplex.shiftFunctor_map_f, NumberField.Units.torsion_eq_one_or_neg_one_of_odd_finrank, surjective_rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar, SpecialLinearGroup.coe_pow, Nat.radical_le_self_iff, map_units_inv, WeierstrassCurve.Projective.negMap_of_Z_ne_zero, Units.inv_mul_eq_one, Units.mk0_mul, Units.mul_inv_eq_one, NormedRing.inverse_add_norm_diff_second_order, Matrix.SpecialLinearGroup.toLin_equiv.symm_toLinearMap_eq, WeierstrassCurve.Projective.nonsingularLift_iff, FiniteField.unit_isSquare_iff, Nat.sum_divisors_filter_squarefree, Module.stabilizer_units_eq_bot_of_ne_zero, HahnSeries.binomial_power, Commute.units_zpow_left, MonoidWithZeroHom.inr_mono, ZMod.isCyclic_units_of_prime_pow, pinGroup.conjAct_smul_range_ι, Submonoid.units_inf, WeierstrassCurve.VariableChange.one_def, Nat.card_eq_card_units_add_one, NumberField.Units.dirichletUnitTheorem.logEmbedding_eq_zero_iff, cfc_zpow, Equiv.Perm.signAux3_mul_and_swap, CStarAlgebra.one_le_inv_iff_le_one, IsCyclotomicExtension.Rat.galEquivZMod_restrictNormal_apply, HomologicalComplex₂.ι_totalShift₂Iso_hom_f_assoc, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₁, LaurentPolynomial.eval₂_C_mul_T_neg_n, Matrix.charpoly_units_conj, ContinuousLinearEquiv.toLinearEquiv_smul, val_unitsCentralizerEquiv_symm_apply_coe, Equiv.Perm.sign_symm_trans_trans, Units.mul_inv_cancel_left, Submodule.unitsQuotEquivRelPic_symm_apply, Subgroup.ofUnits_mono, IsPrimitiveRoot.isUnit_unit', Equiv.Perm.mem_ofSign, MulChar.ofUnitHom_eq, Matrix.SpecialLinearGroup.range_toGL, Units.smul_inv, ComplexShape.ε_zero, Subgroup.ofUnits_inf_units, Subgroup.val_centerUnitsEquivUnitsCenter_apply_coe, WeierstrassCurve.Jacobian.nonsingularLift_zero, Projectivization.exists_smul_eq_mk_rep, ContinuousLinearEquiv.unitsEquivAut_symm_apply, Units.val_neg, MonoidWithZeroHom.snd_inr, MonoidWithZeroHom.snd_inl_apply_of_ne_zero, IsValuativeTopology.hasBasis_nhds, one_divp, HomologicalComplex.mapBifunctor₂₃.d₁_eq, WithZero.toMonoidWithZeroHom_withZeroUnitsEquiv, AlgEquiv.algHomUnitsEquiv_apply_symm_apply, AddConstEquiv.coe_val_inv_equivUnits_apply, Int.negOnePow_two_mul_add_one, Units.continuous_iff, cfc_inv_id, isQuotientCoveringMap_zpow, Commute.units_inv_left, AlgEquiv.val_algHomUnitsEquiv_symm_apply, CircleDeg1Lift.coe_toOrderIso, CircleDeg1Lift.translate_zpow, CategoryTheory.CatCenter.smul_iso_inv_eq_assoc, CochainComplex.HomComplex.Cochain.shift_units_smul, RingPreordering.unitsInv_mem, MonoidWithZeroHom.inl_injective, WeierstrassCurve.Projective.addMap_of_Y_eq, HahnSeries.pow_add, ClassGroup.mk_mk0, NumberField.IsCMField.unitsMulComplexConjInv_ker, Unitary.toRingEquiv_conjStarAlgAut, CochainComplex.ι_mapBifunctorShift₂Iso_hom_f, Unitary.val_toUnits_apply, Ring.inverse_unit, instContinuousStarUnits, divp_one, HomologicalComplex₂.D₁_totalShift₁XIso_hom, Complex.linearEquiv_det_conjAe, Units.val_smul, HomologicalComplex₂.D₂_totalShift₁XIso_hom, Int.units_eq_one_or, TotalComplexShapeSymmetry.σ_ε₂, Matrix.submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det', nnnorm_units_zsmul, IsValuativeTopology.hasBasis_nhds_zero, ValuationSubring.unitGroup_le_unitGroup, uzpow_add, WeierstrassCurve.variableChange_Δ, IsCyclotomicExtension.Rat.Three.Units.mem, NumberField.Units.complexEmbedding_apply, ContinuousLinearEquiv.unitsEquivAut_apply_symm, ValuationSubring.principal_units_le_units, rootsOfUnity_inf_rootsOfUnity, ClassGroup.mk_eq_one_iff, MultilinearMap.alternatization_apply, WeierstrassCurve.coe_inv_map_Δ', pinGroup.toUnits_injective, divp_divp_eq_divp_mul, WeierstrassCurve.variableChange_a₄, val_inv_cfcUnits, isGroupLikeElem_unitsInv, Valuation.IsRankOneDiscrete.generator_zpowers_eq_valueGroup, WeierstrassCurve.Projective.negMap_eq, pinGroup.units_mem_lipschitzGroup, toPrincipalIdeal_eq_iff, PowerSeries.map_invUnitsSub, Algebra.smul_units_def, ComplexShape.σ_ε₂, NumberField.Units.coe_pow, Units.embedding_val_mk, ContinuousMap.continuous_isUnit_unit, SpecialLinearGroup.centerEquivRootsOfUnity_apply, Equiv.Perm.decomposeOption_symm_sign, WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal', CStarAlgebra.inv_le_inv, LinearEquiv.smul_apply, AffineEquiv.equivUnitsAffineMap_symm_apply_symm_apply, CochainComplex.HomComplex.Cochain.units_smul_v, ConjAct.units_continuousConstSMul, NumberField.IsCMField.unitsMulComplexConjInv_apply, CochainComplex.HomComplex.Cochain.δ_toSingleMk, IsCompactOperator.smul_unit_iff, Set.unit_valuation_eq_one, Units.continuousConstSMul, HasDerivAt.hasFDerivAt_equiv, unitsEquivNeZero_apply_coe, Matrix.detp_smul_adjp, Units.smulCommClass', HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₂, Units.isEmbedding_val, Units.coe_inv_smul, GroupLike.val_toUnits_apply, LinearEquiv.toLinearMap_smul, ClassGroup.mk_eq_mk, Units.neg_smul, CategoryTheory.Functor.map_units_smul, Unitary.val_inv_toUnits_apply, Units.topology_eq_inf, hasStrictFDerivAt_ringInverse, LinearOrderedCommGroupWithZero.inr_eq_coe_inrₗ, HNNExtension.NormalWord.empty_toList, AddConstEquiv.equivUnits_symm_apply_apply, pinGroup.mem_lipschitzGroup, PowerSeries.invOneSubPow_add, NumberField.Units.coe_injective, NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociates_eq_iff, NumberField.mixedEmbedding.logMap_unit_smul, NumberField.Units.coe_one, WeierstrassCurve.Jacobian.addMap_of_Z_eq_zero_left, WithZero.logEquiv_apply, units_eq_one, Equiv.Perm.sign_permCongr, spectrum.map_inv, CochainComplex.HomComplex.Cochain.rightShift_units_smul, Unitary.toUnits_comp_map, ClassGroup.equivPic_symm_apply, LocalizedModule.lift_mk, Continuous.units_map, Units.eq_inv_of_mul_eq_one_right, NumberField.IsCMField.mem_realUnits_iff, CategoryTheory.CatCenter.smul_iso_hom_eq_assoc, LinearOrderedCommGroupWithZero.fst_comp_inl, Units.instT2Space, isOpenUnits_iff, WeierstrassCurve.Projective.addMap_of_Z_eq_zero_right, IsLocalRing.surjective_units_map_of_local_ringHom, mem_skewAdjointMatricesLieSubalgebra_unit_smul, NumberField.mixedEmbedding.unitSMul_smul, Int.negOnePow_sub, one_uzpow, Units.conj_pow, Nat.prime_iff_card_units, ContinuousMap.canLift, ContinuousMultilinearMap.alternatization_apply_toContinuousMultilinearMap, Units.one_le_inv_mul_of_le, ZMod.unitsMap_val, AffineEquiv.equivUnitsAffineMap_symm_apply_toFun, ZMod.isCyclic_units_four, Commute.units_inv_right, NumberField.IsCMField.unitsComplexConj_eq_self_iff, Matrix.exp_units_conj', Submonoid.LocalizationMap.lift_apply, HNNExtension.toSubgroupEquiv_neg_apply, ValuationSubring.surjective_unitGroupToResidueFieldUnits, Units.smul_def, MonoidWithZeroHom.snd_mono, WeierstrassCurve.Affine.Point.toClass_some, CochainComplex.HomComplex.Cochain.δ_shift, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₃, Units.inv_mul_eq_inv_mul_iff, ValuationSubring.principalUnitGroupEquiv_apply, Algebra.SubmersivePresentation.aeval_invJacobianOfHasCoeffs, LucasLehmer.order_ω, MonCat.val_units_map_hom_apply, HomologicalComplex₂.totalShift₁Iso_trans_totalShift₂Iso, Subgroup.HasDetPlusMinusOne.det_eq, Submonoid.mem_units_iff, Units.isScalarTower', CochainComplex.HomComplex.Cochain.comp_units_smul, IsDedekindDomain.selmerGroup.fromUnit_ker, Module.Basis.det_inv, linearEquiv_det_rotation, Matrix.GeneralLinearGroup.val_inv_det_apply, Matrix.GeneralLinearGroup.center_eq_range_units, Subgroup.unit_mem_of_mem_ofUnits, IsUnit.val_inv_unit', Polynomial.coeff_inv_units, HomologicalComplex₂.d₂_eq, HNNExtension.NormalWord.unitsSMul_neg, ZMod.natCast_smul_units, Valuation.instNontrivialSubtypeUnitsMemSubgroupValueGroupOfIsNontrivial, MonoidWithZeroHom.fst_apply_coe, LaurentPolynomial.smeval_single, MonoidWithZeroHom.fst_inl, MonoidWithZeroHom.fst_surjective, Units.toMulEquiv_mapContinuousMulEquiv, Units.eq_mul_inv_iff_mul_eq, CircleDeg1Lift.translationNumber_conj_eq, ValuativeRel.isNontrivial_iff_nontrivial_units, Matrix.SpecialLinearGroup.eq_scalar_center_equiv_rootsOfUnity, MonoidWithZeroHom.valueGroup_def, Fintype.card_units_int, Matrix.detp_smul_add_adjp, instFiniteZModUnits, Units.inv_mul_of_eq, CFC.rpow_intCast, CategoryTheory.CatCenter.smul_iso_inv_eq, Matrix.SpecialLinearGroup.coe_to_GLPos_to_GL_det, Units.val_set_image_rootsOfUnity_two, ValuationSubring.mem_principalUnitGroup_iff, Units.add_eq_mul_one_add_div, CategoryTheory.CatCenter.app_neg_one_zpow, Commute.units_val_iff, ComplexShape.eulerCharSignsUpNat_χ, ContinuousLinearEquiv.conjContinuousAlgEquiv_ext_iff, Module.Basis.map_orientation_eq_det_inv_smul, instFiniteUnits, Units.map_comp, CochainComplex.HomComplex.Cochain.δ_rightUnshift, Units.inv_mul_cancel_right, Int.negOnePow_zero, Polynomial.newtonMap_apply_of_isUnit, IsDedekindDomain.HeightOneSpectrum.valuationOfNeZero_eq, Units.eq_one, Matrix.det_mul_aux, MonoidWithZeroHom.snd_comp_inr, Int.units_sq, NumberField.Units.dirichletUnitTheorem.logEmbedding_component, CochainComplex.HomComplex.Cochain.leftUnshift_units_smul, NumberField.Units.coe_zpow, Matrix.isAddUnit_detp_smul_mul_adjp, MonoidWithZeroHom.valueMonoid_eq_closure, Matrix.detp_mul, Valued.integer.locallyFiniteOrder_units_mrange_of_isCompact_integer, Algebra.SubmersivePresentation.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one, Matrix.GeneralLinearGroup.val_inv_scalar_apply, spectrum.units_conjugate', ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply, MulChar.card_eq_card_units_of_hasEnoughRootsOfUnity, SemiconjBy.units_inv_symm_left_iff, IsDedekindDomain.selmerGroup.fromUnitLift_injective, Asymptotics.IsBigOWith.const_mul_right', LinearEquiv.smulOfNeZero_symm_apply, AffineEquiv.coe_homothetyUnitsMulHom_apply, NumberField.Units.logEmbeddingQuot_injective, WeierstrassCurve.Projective.Point.zero_def, IsPrimitiveRoot.isUnit_unit, NumberField.mixedEmbedding.unit_smul_eq_zero, Matrix.det_permute', FiniteField.sum_pow_units, cyclotomicCharacter.toZModPow_toFun, LinearEquiv.trans_smul, GradedTensorProduct.comm_coe_tmul_coe, ValuationSubring.coe_unitGroupMulEquiv_symm_apply, MonoidWithZeroHom.inr_apply_unit, CochainComplex.HomComplex.Cochain.δ_rightShift, MonoidWithZeroHom.valueMonoid_eq_valueGroup', ComplexShape.Associative.ε₂_eq_mul, HomologicalComplex₂.ι_totalShift₂Iso_inv_f, Matrix.mem_glpos, AlgEquiv.val_inv_algHomUnitsEquiv_symm_apply, Ideal.torsionMapQuot_injective, CochainComplex.HomComplex.Cochain.leftShift_v, Units.continuous_coe_inv, pinGroup.mem_iff, MvPowerSeries.coeff_invOfUnit, LinearOrderedCommGroupWithZero.fst_apply, LinearIndependent.units_smul, Units.isClosedEmbedding_embedProduct, Matrix.submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det, CategoryTheory.TwistShiftData.shiftFunctorAdd'_inv_app, CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₃, LaurentPolynomial.eval₂_T_neg_n, SemiconjBy.units_of_val, Units.le_inv_mul_of_mul_le, Submonoid.instSubsingletonUnits, HomologicalComplex.mapBifunctorMapHomotopy.comm₁_aux, Polynomial.det_taylorLinearEquiv, UpperHalfPlane.det_J, CommMonCat.units_obj_coe, Units.mulRight_symm, ComplexShape.Associative.ε₁_eq_mul, Units.val_one, IsCyclic.mulAutMulEquiv_symm_apply_symm_apply, MultilinearMap.alternatization_coe, Units.isEmbedding_val₀, CochainComplex.HomComplex.Cochain.δ_leftUnshift, AffineSubspace.affineSpan_pair_parallel_iff_exists_unit_smul, WeierstrassCurve.Projective.negMap_of_Z_eq_zero, Units.val_injective, HomologicalComplex₂.ιTotal_totalFlipIso_f_hom, Units.toAut_inv, UniqueFactorizationMonoid.primeFactors_eq_natPrimeFactors, Units.inv_neg, PowerSeries.invOneSubPow_eq_inv_one_sub_pow, Int.negOnePow_even, CategoryTheory.CatCenter.smul_iso_hom_eq', FiniteField.unitsMap_norm_surjective, ComplexShape.χ_next, modularCyclotomicCharacter.comp, NormalizationMonoid.normUnit_mul, ArithmeticFunction.carmichael_eq_exponent', ZMod.not_isCyclic_units_eight, WeierstrassCurve.Projective.addMap_of_Z_ne_zero, nonZeroDivisorsEquivUnits_apply, HomologicalComplex.mapBifunctor.d₁_eq', AddAut.mulLeft_apply_apply, PowerSeries.IsWeierstrassDivision.isWeierstrassFactorization, divp_inv, Units.coeHom_apply, AlgEquiv.smul_units_def, lipschitzGroup.coe_mem_iff_mem, Equiv.Perm.equivUnitsEnd_symm_apply_symm_apply, Units.commute_iff_mul_inv_cancel_assoc, Units.instFaithfulSMul, NormedRing.inverse_add_norm_diff_first_order, Submonoid.LocalizationMap.mul_inv_right, normUnit_one, uzpow_sub, TensorProduct.tmul_of_gradedMul_of_tmul, MonoidWithZeroHom.fst_inr_apply_of_ne_zero, cyclotomicCharacter.spec, inv_eq_one_divp', HNNExtension.NormalWord.unitsSMulEquiv_symm_apply, inv_eq_one_divp, GroupLike.val_inv_toUnits_apply, ContinuousLinearEquiv.smul_trans, MonoidWithZeroHom.mem_valueGroup_iff_of_comm, IsCyclotomicExtension.Rat.Three.eq_one_or_neg_one_of_unit_of_congruent, CochainComplex.shiftFunctor_obj_d', MonCat.val_inv_units_map_hom_apply, toUnits_symm_apply, Units.coe_opEquiv_symm, Matrix.SpecialLinearGroup.toLin_equiv.toLinearMap_eq, Units.continuous_embedProduct, FractionalIdeal.spanSingleton_eq_spanSingleton, Submonoid.units_iInf₂, OrderIso.withZeroUnits_apply, ModularForm.prod_fintype_slash, rootsOfUnity_le_of_dvd, Subgroup.val_mem_ofUnits_iff_mem, Units.continuous_map, Set.subset_center_units, ContinuousLinearEquiv.smul_apply, TensorProduct.CompatibleSMul.unit, nnnorm_commutator_units_sub_one_le, rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar_val, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom_assoc, WeierstrassCurve.coe_variableChange_Δ', uzpow_intCast, Equiv.Perm.sign_extendDomain, Fintype.card_eq_card_units_add_one, nonZeroDivisorsEquivUnits_symm_apply_coe, Set.center_units_eq, WithZero.withZeroUnitsEquiv_symm_apply, HNNExtension.toSubgroupEquiv_one, ArithmeticFunction.carmichael_eq_exponent, NumberField.Units.instFGUnitsRingOfIntegers, CochainComplex.HomComplex.Cochain.leftShift_units_smul, Units.instMulArchimedean, WeierstrassCurve.map_Δ', HNNExtension.ReducedWord.map_fst_eq_and_of_prod_eq, WeierstrassCurve.Jacobian.Point.zero_point, MonoidWithZeroHom.inr_strictMono, HNNExtension.NormalWord.cons_toList, LinearEquiv.coe_inv_det, HomologicalComplex.ι_mapBifunctorFlipIso_hom, LinearIndependent.units_smul_iff, IsLocalizedModule.fromLocalizedModule'_mk, Valued.hasBasis_uniformity, ModularForm.slash_def, rootsOfUnityEquivNthRoots_apply, MulChar.trivial_apply, Polynomial.natDegree_of_mem_normalizedFactors_cyclotomic, Subgroup.ofUnits_injective, pinGroup.involute_act_ι_mem_range_ι, Prod.instSubsingletonUnits, NumberField.IsCMField.indexRealUnits_eq_two_iff, card_rootsOfUnity_eq_iff_exists_isPrimitiveRoot, CochainComplex.mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso, Equiv.Perm.equivUnitsEnd_symm_apply_apply, rootsOfUnityCircleEquiv_apply, Units.one_le_mul_inv, Module.Basis.orientation_unitsSMul, toUnits_val_apply, Complex.card_rootsOfUnity, spectrum.preimage_units_mul_comm, Subgroup.ofUnits_iSup₂, FractionalIdeal.map_canonicalEquiv_mk0, Matrix.mul_adjp_apply_ne, Matrix.det_neg_eq_smul, Polynomial.orderOf_root_cyclotomic_dvd, Units.one_le_inv_mul, rootsOfUnity.integer_power_of_ringEquiv', sign_finRotate, ArithmeticFunction.inv_zetaUnit, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₁_assoc, Units.embed_product_star, Equiv.Perm.IsCycle.sign, IsPrimitiveRoot.autToPow_spec, LaurentPolynomial.smeval_C_mul_T_n, Equiv.Perm.sign_inv, MonCat.units_obj_coe, ZMod.isCyclic_units_two, map_zsmul_unit, Submonoid.LocalizationMap.mul_inv_left, MulChar.coe_toUnitHom, IsCyclic.mulAutMulEquiv_symm_apply_apply, ClassGroup.mk_eq_one_of_coe_ideal, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₃, uzpow_neg, norm_commutator_units_sub_one_le, DirichletCharacter.factorsThrough_iff_ker_unitsMap, HomologicalComplex.mapBifunctor.d₂_eq', Units.le_inv_mul_iff, Equiv.Perm.IsThreeCycle.sign, WeierstrassCurve.Jacobian.Point.zero_def, IsUnit.unit_pow, NumberField.Units.logEmbeddingEquiv_apply, IsUnit.unit_one, toPrincipalIdeal_def, Subgroup.mem_iff_toUnits_mem_units, AlternatingMap.domDomCongr_perm, HomologicalComplex₂.ι_totalShift₂Iso_hom_f, NumberField.Units.isMaxRank_iff_closure_finiteIndex, NumberField.Units.exist_unique_eq_mul_prod, Units.contMDiff_val, Units.val_eq_one, IsOfFinOrder.val_inv_unit, Subgroup.unit_of_mem_ofUnits_spec_mem, Equiv.Perm.IsSwap.sign_eq, Submodule.mulExact_unitsMap_spanSingleton_unitsToPic, TensorProduct.gradedCommAux_lof_tmul, Nat.one_lt_radical_iff, MonoidHom.restrict_surjective, NumberField.Units.rootsOfUnity_eq_one, WeierstrassCurve.inv_map_Δ', MonoidWithZeroHom.one_mem_valueMonoid, instCanLiftUnitsValIsUnit, Int.units_ne_iff_eq_neg, Units.orbitRel_nonZero_iff, AffineEquiv.val_inv_equivUnitsAffineMap_apply, CategoryTheory.NatTrans.app_units_zsmul, spectrum.inv₀_mem_inv, LinearMap.trace_conj, IsUnit.val_inv_apply, SemiconjBy.units_zpow_right, autEquivRootsOfUnity_apply_rootOfSplit, Units.coe_star_inv, HahnSeries.coeff_toOrderTopSubOnePos_pow, SemiconjBy.units_val_iff, Equiv.Perm.sign_prodCongrRight, PowerSeries.invOneSubPow_val_one_eq_invUnitSub_one, CochainComplex.mappingCone.δ_descCochain, SpecialLinearGroup.centerEquivRootsOfUnity_apply_apply, CircleDeg1Lift.translationNumber_conj_eq', MonoidWithZeroHom.inl_mono, AddConstEquiv.equivUnits_symm_apply_symm_apply, Units.val_pow_eq_pow_val, rootsOfUnity.coe_pow, restrictRootsOfUnity_coe_apply, Matrix.det_units_conj, LinearEquiv.symm_smul_apply, Subgroup.ofUnits_sSup, HasEnoughRootsOfUnity.finite_rootsOfUnity, CircleDeg1Lift.translationNumber_translate, AddAut.mulLeft_apply_symm_apply, Equiv.Perm.sign_eq_sign_of_equiv, NumberField.Units.finiteIndex_iff_sup_torsion_finiteIndex, HomologicalComplex₂.d₂_eq', WeierstrassCurve.Jacobian.smul_eq, Equiv.Perm.sign_one, MulChar.ofUnitHom_coe, Matrix.SpecialLinearGroup.det_mapGL, Submonoid.unit_mem_leftInv, ZMod.isCyclic_units_two_pow_iff, Subgroup.HasDetPlusMinusOne.abs_det, Units.val_lt_val, CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₂, IsPrimitiveRoot.val_inv_toRootsOfUnity_coe, mem_rootsOfUnity', ClassGroup.equiv_mk0, ComplexShape.ε₂_def, CircleDeg1Lift.translationNumber_units_inv, Subgroup.ofUnits_right_inverse, MonoidWithZeroHom.mem_valueMonoid_iff, Units.le_mul_inv_iff, Submonoid.LocalizationMap.mul_inv, ContinuousMap.unitsLift_symm_apply_apply_inv', ZMod.isCyclic_units_zero, IsGroupLikeElem.unitsInv, WeierstrassCurve.Jacobian.addMap_eq, NumberField.Units.instFiniteIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, HomologicalComplex₂.d₁_eq', Matrix.trace_units_conj', SemiconjBy.units_inv_symm_left, card_rootsOfUnity, spectrum.inv_mem_resolventSet, Units.continuousSMul, Units.divp_sub_divp, DirichletCharacter.Odd.toUnitHom_eval_neg_one, MonoidWithZeroHom.inv_mem_valueGroup, divp_mul_divp, LinearEquiv.smul_trans, Units.inv_le_one_of_le, Nat.divisors_filter_squarefree, Matrix.det_apply', Lagrange.nodal_subgroup_eq_X_pow_card_sub_one, ModularGroup.det_coe, FiniteField.sum_subgroup_units, Module.Basis.orientation_neg_single, Equiv.Perm.sign_prod_list_swap, Units.inv_mul_eq_iff_eq_mul, spectrum.unit_smul_eq_smul, ValuationSubring.ker_unitGroupToResidueFieldUnits, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₁, WithZero.withZeroUnitsEquiv_apply, NormedRing.inverse_add_nth_order, Matrix.GeneralLinearGroup.val_inv_swap, Units.mk0_prod, Submonoid.LocalizationMap.lift₀_apply, Valuation.ltIdeal_mono, MulChar.apply_mem_rootsOfUnity_orderOf, Circle.toUnits_apply, mul_uzpow, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₃, ClassGroup.mk_canonicalEquiv, HomologicalComplex₂.D₁_totalShift₂XIso_hom, IsUnit.val_inv_mul, Nonneg.val_inv_unitsEquivPos_symm_apply_coe, Matrix.GeneralLinearGroup.val_scalar_apply, val_rootsOfUnityEquivOfPrimitiveRoots_apply_coe, Units.eq_inv_of_mul_eq_one_left, Equiv.Perm.sign_prodCongrLeft, MonoidWithZeroHom.snd_apply_coe, HomologicalComplex.mapBifunctor₁₂.d₁_eq, IsUnit.liftRight_inv_mul, HomologicalComplex₂.D₂_totalShift₂XIso_hom, ClassGroup.equivPic_apply, Submonoid.val_unitsTypeEquivIsUnitSubmonoid_symm_apply, IsDedekindDomain.HeightOneSpectrum.valuation_of_unit_mod_eq, MonoidHom.toHomUnitsMulEquiv_symm_apply, MulEquiv.val_piUnits_apply, Units.mulArchimedean_iff, norm_units_zsmul, WeierstrassCurve.Jacobian.negMap_eq, Module.Basis.repr_unitsSMul, Submonoid.IsUnit.Submonoid.coe_inv, MulChar.coe_equivToUnitHom, LinearEquiv.det_refl, spectrum.units_smul_resolvent, ZMod.isCyclic_units_prime, Units.mul_inv_le_of_le_mul, invOf_units, HomologicalComplex.mapBifunctor₁₂.d₃_eq, Equiv.Perm.sign_of_cycleType', Units.smul_eq_mul, NumberField.Units.regulator_eq_det', Equiv.Perm.sign_subtypeCongr, HasStrictDerivAt.hasStrictFDerivAt_equiv, Subgroup.ofUnits_iSup, Matrix.exp_units_conj, LinearOrderedCommGroupWithZero.inl_apply, SpecialLinearGroup.baseChange_apply_coe, Units.isOpenEmbedding_val, Unitization.val_unitsFstOne_mulEquiv_quasiregular_apply, LinearOrderedCommGroupWithZero.inr_apply, NormedSpace.exp_units_conj, HNNExtension.NormalWord.ofGroup_toList, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₁, Nat.radical_le_one_iff, CategoryTheory.CatCenter.smul_iso_hom_eq, Polynomial.normUnit_X, PowerSeries.IsWeierstrassDivisorAt.seq_one, autAdjoinRootXPowSubC_root, CategoryTheory.CommShift₂Setup.z_zero₂, CategoryTheory.CommShift₂Setup.int_ε, NumberField.Units.dirichletUnitTheorem.logEmbedding_ker, Module.Basis.units_smul_span_eq_top, Equiv.Perm.ofSign_disjUnion, TensorProduct.gradedComm_of_tmul_of, Subgroup.mem_units_iff_val_mem, exteriorPower.toTensorPower_apply_ιMulti, Units.chartAt_source, Equiv.Perm.prod_Iio_comp_eq_sign_mul_prod, SemiconjBy.units_inv_right_iff, alternatingGroup_eq_sign_ker, NumberField.IsCMField.map_unitsMulComplexConjInv_torsion, HomologicalComplex.mapBifunctor₁₂.d₂_eq, Polynomial.roots_C_mul_X_add_C_of_IsUnit, Module.Basis.unitsSMul_apply, Int.negOnePow_succ, HahnSeries.val_toOrderTopSubOnePos_coe, WeierstrassCurve.variableChange_c₄, LinearEquiv.smul_refl, Module.Basis.coord_unitsSMul, Equiv.optionCongr_sign, HahnSeries.mem_orderTopSubOnePos_iff, rootsOfUnityEquivNthRoots_symm_apply, ZMod.orderOf_units_dvd_card_sub_one, denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units, ZMod.isCyclic_units_four_mul_iff, SpecialLinearGroup.coe_div, NumberField.Units.complexEmbedding_inj, Units.range_embedProduct, Equiv.Perm.val_inv_equivUnitsEnd_apply, MonoidWithZeroHom.inr_injective, HahnSeries.val_inv_toOrderTopSubOnePos_coe, CochainComplex.HomComplex.Cochain.δ_leftShift, HomologicalComplex₂.totalAux.d₁_eq', Unitization.unitsFstOne_val_val_fst, CircleDeg1Lift.translate_pow, Matrix.mul_adjp_add_detp, MonoidWithZeroHom.commute_inl_inr, SemiconjBy.units_inv_right, TotalComplexShape.ε₂_ε₁, MonoidWithZeroHom.fst_comp_inr, Units.commute_iff_mul_inv_cancel, Ring.inverse_of_isUnit, HomologicalComplex.ι_mapBifunctorFlipIso_hom_assoc, Submodule.span_singleton_eq_span_singleton, WeierstrassCurve.variableChange_a₆, Module.Basis.toMatrix_unitsSMul, Valuation.IsRankOneDiscrete.exists_generator_lt_one, Units.embedProduct_injective, HNNExtension.NormalWord.unitsSMulEquiv_apply, Units.eq_inv_mul_iff_mul_eq, NumberField.Units.regOfFamily_eq_det', LinearIsometryEquiv.toContinuousLinearEquiv_smul, Units.isOrderedMonoid, WeierstrassCurve.Jacobian.addMap_of_Y_eq, instSubsingletonSubtypeUnitsMemSubgroupRootsOfUnityOfNatNat, Submodule.mulExact_unitsToPic_mapAlgebra, WithZero.val_logOrderIso_symm_apply, CochainComplex.HomComplex.δ_zero_cochain_comp, Units.isScalarTower'_left, HNNExtension.ReducedWord.toList_eq_nil_of_mem_of_range, NumberField.IsCMField.complexConj_torsion, Units.isOpenMap_val, MulChar.apply_mem_rootsOfUnity, ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk, ZMod.smul_units_def, AddConstEquiv.coe_val_equivUnits_apply, Units.isInducing_embedProduct, Units.coeHom_injective, rootsOfUnityEquivOfPrimitiveRoots_symm_apply, Units.mapContinuousMulEquiv_apply, UpperHalfPlane.smulAux'_im, Matrix.coe_units_zpow, CategoryTheory.CommShift₂Setup.z_zero₁, map_rootsOfUnity, FractionalIdeal.coe_mk0, ClassGroup.mk_def, Equiv.Perm.sign_swap', PowerSeries.derivative_inv, SpecialLinearGroup.coe_dualMap, Units.val_mul, ValuationSubring.coe_unitGroupToResidueFieldUnits_apply, Submonoid.units_mono, Units.inv_mul_le_one, Int.negOnePow_eq_one_iff, CStarAlgebra.inv_le_one_iff_one_le, modularCyclotomicCharacter.aux_spec, Units.one_le_mul_inv_of_le, CategoryTheory.CommShift₂Setup.hε, WeierstrassCurve.Affine.Point.toClass_apply, Polynomial.normalizedFactors_cyclotomic_card, Equiv.Perm.sign_swap, CFC.inv_nonneg_of_nonneg, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₁, HomologicalComplex.mapBifunctor.d₁_eq, Units.mk0_one, WeierstrassCurve.Projective.nonsingularLift_zero, Units.mk_semiconjBy, Module.End.algebraMap_isUnit_inv_apply_eq_iff, WeierstrassCurve.VariableChange.map_u, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₂_assoc, ZMod.rootsOfUnityAddChar_val, val_div_eq_divp, WithZero.logEquiv_unitsMk0, WithZero.val_inv_logOrderIso_symm_apply, Subgroup.ofUnits_sup_units, cyclotomicCharacter.continuous, Equiv.Perm.sign_ofSubtype, Units.coe_mapEquiv, AffineEquiv.equivUnitsAffineMap_symm_apply_invFun, FiniteField.prod_univ_units_id_eq_neg_one, spinGroup.toUnits_injective, Matrix.isAddUnit_detp_mul_detp, ValuationSubring.principalUnitGroup_injective, CircleDeg1Lift.translationNumber_zpow, rootsOfUnity_zero, modularCyclotomicCharacter.toFun_spec'', NumberField.IsCMField.index_unitsMulComplexConjInv_range_dvd, Submodule.ker_unitsMap_spanSingleton, IsCyclotomicExtension.autEquivPow_symm_apply, Unitization.mem_unitsFstOne, SpecialLinearGroup.toLinearEquiv_to_linearMap, WithZero.unitsWithZeroEquiv_apply, AlgEquiv.algHomUnitsEquiv_apply_apply, Units.mul_eq_one_iff_inv_eq, cyclotomicCharacter.toFun_spec, CochainComplex.shiftFunctor_obj_d, HNNExtension.ReducedWord.exists_normalWord_prod_eq, Units.map_neg_one, SpecialLinearGroup.centerEquivRootsOfUnity_apply_of_finrank_le_one, ClassGroup.equiv_mk, cfc_comp_inv, MonoidWithZeroHom.inl_apply_unit, MonoidWithZeroHom.snd_surjective, Units.inv_mul_mem_unitary, IsDedekindDomain.selmerGroup.valuation_ker_eq, MultilinearMap.alternatization_def, natCard_units_lt, CategoryTheory.ObjectProperty.smul_mem_trW_iff, Unitization.unitsFstOne_val_inv_val_fst, ValuationSubring.principalUnitGroup_symm_apply, NumberField.Units.instFreeIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion, Subgroup.hasDetPlusMinusOne_iff_abs_det, WithZero.withZeroUnitsEquiv_strictMono, RootPairing.Equiv.toEndUnit_val, Units.embedProduct_apply, mem_rootsOfUnity_prime_pow_mul_iff, LinearEquiv.coe_det, IsCyclotomicExtension.autEquivPow_apply, val_inv_unitOfInvertible, HomologicalComplex.ι_mapBifunctorFlipIso_inv, Equiv.Perm.signAux_mul, MulEquiv.val_inv_piUnits_symm_apply, Submodule.unitsQuotEquivRelPic_apply_coe, IsPrimitiveRoot.map_rootsOfUnity, MonoidHom.toHomUnitsMulEquiv_apply, Units.chartAt_apply, instDenselyOrderedUnits, spinGroup.val_toUnits_apply, Equiv.Perm.sign_surjective, cfcUnits_zpow, IsCyclotomicExtension.Rat.galEquivZMod_smul_of_pow_eq, EqualCharZero.pnatCast_one, QuadraticForm.equivalent_weightedSumSquares_units_of_nondegenerate', ModularForm.slash_apply, CategoryTheory.CommShift₂Setup.int_z, le_iff_norm_sqrt_mul_sqrt_inv, Int.units_mul_self, Equiv.Perm.OnCycleFactors.sign_kerParam_apply_apply, rootsOfUnity.eq_one, Units.inv_mul_cancel_left, CategoryTheory.TwistShiftData.z_zero_right, ofMul_uzpow, instSmallUnitsSkeletonSemimoduleCat, autEquivRootsOfUnity_smul, Matrix.GeneralLinearGroup.val_det_apply, UpperHalfPlane.petersson_slash, HomologicalComplex₂.ιTotal_totalFlipIso_f_inv, WeierstrassCurve.variableChange_b₄

---

← Back to Index