← all areas

Namespace (no namespace) 98 theorems

Landmarks here: Fermat's Last Theorem · Fermat's Last Theorem for the exponent 5 · Fermat's Last Theorem for exponent 7 · Kummer's theorem: Fermat's Last Theorem for regular primes

• landmark Fermat's Last Theorem fermat_last_theorem 29,488 below · cited by 0 · depth 0
• Fermat's Last Theorem for exponent 11 fermatLastTheoremEleven 2 below · cited by 1 · depth 6
• landmark Fermat's Last Theorem for the exponent 5 fermatLastTheoremFive 0 below · cited by 1 · depth 6
• landmark Fermat's Last Theorem for exponent 7 fermatLastTheoremSeven 2 below · cited by 1 · depth 6
• Fermat's Last Theorem for exponent 13 fermatLastTheoremThirteen 2 below · cited by 1 · depth 6
• landmark Kummer's theorem: Fermat's Last Theorem for regular primes flt_regular 0 below · cited by 3 · depth 7
• Power sums of ζ^k/(1-ζ^k)² over half the p-th roots cyclotomic_velu_powerSums 0 below · cited by 2 · depth 8
• Vélu's x-map for μₚ on the split node cyclotomic_velu_xLaw 0 below · cited by 1 · depth 8
• Embedding a ℤ-finite domain into a complete DVR exists_ringHom_completeDVR_residue_eq_of_moduleFinite_int 3 below · cited by 1 · depth 9
• Integer-valued sequences near polynomial branches are polynomial on progressions exists_polynomial_eq_on_arithProg 0 below · cited by 1 · depth 10
• Integral complex numbers lie in the integral closure of ℤ exists_integralClosure_coe_eq_of_isIntegral 0 below · cited by 1 · depth 11
• The chosen place of ℚ̄ above p lies over p padicPlace_liesOverPrime 0 below · cited by 8 · depth 11
• Determinant of a Frobenius-normalised stable plane is integrally cyclotomic eigenPlane_det_congruent_cyclotomic_of_frobenius_det 486 below · cited by 9 · depth 12
• Frobenius determinant equals ℓ on a Hecke eigenplane eigenPlane_det_frobenius_eq_prime 1,037 below · cited by 9 · depth 12
• Inertia at ℓ moves some ℓ-power roots of unity exists_inertiaSubgroupIn_rootOfUnity_pow_ne_one 2 below · cited by 10 · depth 12
• Northcott's theorem for projective space over a number field northcott_projMulHeight_numberField 0 below · cited by 1 · depth 12
• Krull dimension does not increase along an integral homomorphism ringKrullDim_le_of_ringHom_isIntegral 0 below · cited by 14 · depth 13
• Descent of a residual representation to Gal(L₀/ℚ) exists_residualRep_descent 0 below · cited by 1 · depth 14
• q dj/dq · Δ = -E₄²E₆ as q-expansions omegaRow_T2 87 below · cited by 10 · depth 14
• Multiplicativity of torsion cardinalities in a divisible abelian group card_torsion_mul_of_divisible 0 below · cited by 2 · depth 15
• Global levels are cofinal among finite local levels exists_finiteDimensional_comap_localGaloisToGlobal_iff 4 below · cited by 15 · depth 15
• Étale descent of regularity to localizations at primes isRegularLocalRing_localization_atPrime_of_etale_of_comap 0 below · cited by 2 · depth 15
• Standard-smooth algebras over a field have regular local localizations isRegularLocalRing_localization_atPrime_of_isStandardSmooth 3 below · cited by 2 · depth 15
• Degree of a primitive m-th root of unity over a finite field minpoly_natDegree_eq_orderOf_of_isPrimitiveRoot 0 below · cited by 2 · depth 15
• Rademacher's congruence for Φ at level ℓ rademacher_phi_level_congruence 0 below · cited by 2 · depth 15
• Connected component of (A∩ B)ᶜ through a point of A∖ B connectedComponentIn_compl_inter_eq_of_isClosed_of_union_eq_univ 0 below · cited by 2 · depth 16
• Localisations of k[X₁,…,Xₙ] at primes are regular local isRegularLocalRing_localization_atPrime_mvPolynomial 0 below · cited by 1 · depth 16
• Local-to-global restriction and fixing subgroups of ℚ_q(ι F) localGaloisToGlobal_mem_fixingSubgroup_iff 0 below · cited by 8 · depth 16
• Dedekind-sum phase identity at levels ≡ 109 (mod 120) rademacher_phi_level_witness_mod_oneTwenty_eq_oneHundredNine 3 below · cited by 1 · depth 16
• Dedekind-sum phase witness at levels ≡ 61 (mod 120) rademacher_phi_level_witness_mod_oneTwenty_eq_sixtyOne 4 below · cited by 1 · depth 16
• Rademacher's Φ under an ST^q-step rademacher_phi_step 0 below · cited by 2 · depth 16
• Finite flat algebras over a PID have local dimension one ringKrullDim_localization_eq_one_of_isPrincipalIdealRing_of_flat 0 below · cited by 1 · depth 16
• Dedekind's reciprocity law for s(h,k)+s(k,h) dedekindSum_add_dedekindSum 0 below · cited by 5 · depth 17
• Dedekind's congruence modulo 8 for 12k s(h,k) dedekindSum_jacobiSym_mod_eight 2 below · cited by 1 · depth 17
• Oddness of the Dedekind sum: s(k-1,k)=-s(1,k) dedekindSum_natCast_sub_one 0 below · cited by 3 · depth 17
• Invariance of s(h,k) under inversion modulo k dedekindSum_of_mul_modEq_one 0 below · cited by 1 · depth 17
• Closed form s(1,k)=(k-1)(k-2)/(12k) dedekindSum_one_left 0 below · cited by 4 · depth 17
• Uniform Schwartz bounds for compact families of affine pullbacks exists_isCompact_tsupport_subset_and_norm_pow_mul_norm_iteratedFDeriv_comp_le_of_hasCompactSupport 0 below · cited by 2 · depth 17
• A q-th root of unity close to 1 is trivial near V(p) exists_sub_one_mem_span_and_mul_sub_one_eq_zero_of_pow_eq_one_of_sub_one_mem_span_pow 0 below · cited by 1 · depth 17
• Dedekind-sum witness for levels ℓ ≡ 11 (mod 12) rademacher_phi_level_witness_eleven 0 below · cited by 1 · depth 17
• Rademacher Φ witness for ℓ≡ 5(mod 12) rademacher_phi_level_witness_five 0 below · cited by 1 · depth 17
• A Dedekind-sum phase identity at levels ≡ 49 (mod 120) rademacher_phi_level_witness_mod_oneTwenty_eq_fortyNine 3 below · cited by 1 · depth 17
• Dedekind-sum witness identity at levels ≡ 1 (mod 120) rademacher_phi_level_witness_mod_oneTwenty_eq_one 2 below · cited by 1 · depth 17
• Rademacher Φ witness for ℓ≡ 13(mod 60) rademacher_phi_level_witness_mod_sixty_eq_thirteen 0 below · cited by 1 · depth 17
• Dedekind-sum level witness for ℓ ≡ 37 (mod 60) rademacher_phi_level_witness_mod_sixty_eq_thirtySeven 0 below · cited by 1 · depth 17
• Dedekind-sum witness for levels ℓ≡ 7(mod 12) rademacher_phi_level_witness_seven 0 below · cited by 1 · depth 17
• |G₀| = e for Galois Dedekind local extensions card_lowerRamificationGroup_zero_eq_ramificationIdxIn 0 below · cited by 1 · depth 18
• Fundamental cycles of a spanning tree generate all flows exists_fundamentalCycles_of_spanningTree 0 below · cited by 2 · depth 18
• Integrality of 6k s(h,k) for Dedekind sums exists_intCast_eq_six_mul_dedekindSum 0 below · cited by 1 · depth 18
• Order of Q modulo Qⁿ-1 equals n orderOf_unitOfCoprime_pow_sub_one 0 below · cited by 2 · depth 18
• Vanishing second differences force an affine sequence eq_add_sub_mul_natCast_of_sub_two_mul_add_eq_zero 0 below · cited by 1 · depth 19
• Uniform bound |logμ(x)|≤ c (-logμ(p)) for algebraic x exists_abs_log_abv_le_mul_neg_log_of_isAlgebraic 0 below · cited by 4 · depth 19
• 1+M consists of units when M is closed, multiplicative and of norm <1 exists_mem_addSubgroup_one_add_mul_one_add_eq_one 0 below · cited by 1 · depth 19
• Completeness of the unit filtration attached to a shrinking chain of additive subgroups exists_units_forall_div_sub_one_mem 0 below · cited by 1 · depth 19
• Norm expansion N(1+γ)=1+Tr γ+Nγ+Tr δ in prime degree prod_one_add_smul_eq_one_add_finsum_add_finprod_add_finsum_smul_of_prime_card 0 below · cited by 3 · depth 19
• Decomposition of a group element into p'- and p-parts exists_commute_mul_eq_orderOf_coprime_pow_prime_pow_eq_one 0 below · cited by 1 · depth 20
• Four-dimensional central division ℚ-algebras are quaternion algebras exists_nonempty_algEquiv_quaternionAlgebra_of_finrank_eq_four 0 below · cited by 1 · depth 20
• ℚ⊗ O is a quaternion division algebra with centre ℚ finrank_rat_tensorProduct_eq_four_and_forall_isUnit_and_forall_comm_mem_range 0 below · cited by 1 · depth 20
• Jacobi triple product for vartheta₂(z,τ) jacobiTheta_two_eq_tprod 0 below · cited by 2 · depth 20
• Legendre parameters over j=0 and j=1728 are q²-fixed pow_sq_eq_self_of_level_two_value_of_eq_zero_or_eq_1728 0 below · cited by 6 · depth 20
• Real Tate integrals of Gaussian times polynomial: Γ_ℝ-factorisation exists_entire_tateIntegral_polyGaussLinear_eq_GammaR_mul 1 below · cited by 1 · depth 21
• Integrability of min(1,r)ᵖmax(1,r)^{-q}rᶜ⁻¹ on (0,∞) integrableOn_Ioi_min_one_rpow_mul_max_one_rpow_mul_rpow_sub_one 0 below · cited by 2 · depth 21
• Unisolvent points exist for a linearly independent family exists_det_of_apply_ne_zero_of_linearIndependent 0 below · cited by 1 · depth 22
• Divisibility detected up to a bounded defect exists_forall_eq_pow_smul_of_forall_smul_mem_of_faithful 0 below · cited by 2 · depth 22
• Rational cyclicity gives cyclicity after a bounded power of varpi exists_forall_pow_smul_eq_smul_of_forall_exists_smul_eq_smul 0 below · cited by 1 · depth 22
• Approximate idempotent tower cutting out a maximal ideal over ℓ exists_idempotent_tower_of_finite_quotient_of_isMaximal 0 below · cited by 1 · depth 22
• Inversion of Abel's half-line integral equation, smooth families exists_abelInverse_linear_contDiff_eq_zero_of_le_integral_div_sqrt_sub_eq 0 below · cited by 1 · depth 24
• Orthogonal idempotents from a prime-order endomorphism exists_isIdempotentElem_mul_iterate_eq_zero_sum_iterate_eq_one_of_not_isField 0 below · cited by 1 · depth 24
• A linear Whitney–Hadamard operator, with smooth dependence on parameters exists_linear_contDiff_hasCompactSupport_apply_sq_eq_of_even_of_odd 0 below · cited by 2 · depth 24
• Vanishing of atomic mass on a coordinate fibre tsum_subtype_eq_zero_of_forall_mem_starAlgebra_adjoin_coord_tsum_mul_eq_of_noAtom 0 below · cited by 1 · depth 24
• Unique valuation ring over a totally ramified layer existsUnique_valuationSubring_of_pow_eq_mul 0 below · cited by 3 · depth 25
• Residue field at a maximal ideal as a finite separable extension exists_residueField_of_isMaximal_of_finiteDimensional 0 below · cited by 1 · depth 25
• Spanning tree of a connected finite multigraph exists_spanningTree_of_connected 0 below · cited by 1 · depth 25
• Component-swapping homeomorphism moves a connected component off itself image_connectedComponentIn_subset_diff_of_forall_mem_irreducibleComponents_image_ne 0 below · cited by 1 · depth 25
• Cyclotomic characters agree under restriction to ℚ̄ cyclotomicCharacter_localGaloisToGlobal 0 below · cited by 1 · depth 26
• Unit-root idempotent for an element of a module-finite ℤₚ-algebra exists_idempotent_mul_eq_and_pow_mul_sub_mem_of_moduleFinite_padicInt 2 below · cited by 1 · depth 26
• Vanishing (d+1)-st forward difference characterises numerical polynomials fwdDiff_iter_succ_eq_zero_iff_exists_polynomial_natDegree_le 0 below · cited by 3 · depth 26
• Binomial expansion of (u+p^rv)^{p^n} modulo p^{n+r+1} add_pow_prime_pow_eq_add_mul_add_mul_of_ne_two_or_two_le 0 below · cited by 1 · depth 28
• Binomial expansion of (u+2v)^{2^n} modulo 2ⁿ⁺² add_two_mul_pow_two_pow_eq 0 below · cited by 1 · depth 28
• Globalising a homomorphism defined on a ball exists_unique_monoidHom_multiplicative_eq_of_forall_norm_lt_map_add 0 below · cited by 1 · depth 29
• Unipotent element of order a unit is trivial eq_one_of_isNilpotent_sub_one_of_pow_eq_one 0 below · cited by 1 · depth 32
• Regularity on a nonzero free module detects non-zero-divisors isSMulRegular_iff_of_free 0 below · cited by 1 · depth 32
• Strong (N+1)-st roots of unity make N+1 invertible isUnit_natCast_succ_of_pow_eq_one_of_forall_isUnit_one_sub_pow 0 below · cited by 2 · depth 32
• Smoothness and compact support of an affine-family integral contDiff_top_and_hasCompactSupport_integral_comp_affine 0 below · cited by 2 · depth 33
• Lagrange idempotents for a root of unity over a commutative ring exists_completeOrthogonalIdempotents_mul_eq_pow_mul_of_pow_eq_one_of_forall_isUnit_one_sub_pow 0 below · cited by 3 · depth 33
• Schwarz symmetry for nested derivatives at the origin deriv_deriv_comm_of_contDiffOn 0 below · cited by 1 · depth 34
• Reversing a triple nested derivative of a C³ function deriv_deriv_deriv_reverse_of_contDiffOn 0 below · cited by 1 · depth 34
• Normalised elliptic divisibility sequences satisfy the elliptic relation isEllSequence_normEDS 0 below · cited by 1 · depth 34
• Non-zero-divisor from regularity in all adic completions mem_nonZeroDivisors_of_forall_isMaximal_algebraMap_adicCompletion_mem 0 below · cited by 2 · depth 34
• Krull dimension is invariant under injective integral extensions ringKrullDim_eq_of_injective_of_isIntegral 0 below · cited by 1 · depth 34
• Topological Krull dimension is local on an open cover topologicalKrullDim_eq_iSup_of_isOpen_of_iUnion_eq_univ 0 below · cited by 1 · depth 34
• Maximal ideals of ℤ̄ versus valuation subrings of ℚ̄ exists_valuationSubring_liesOverPrime_forall_mlocal_iff_mem_range 0 below · cited by 1 · depth 36
• Smoothness and derivative bound for x-derivative slices contDiff_iteratedDeriv_slice_and_norm_iteratedFDeriv_le_norm_iteratedFDeriv_add 0 below · cited by 1 · depth 37
• Smooth even Hadamard factorisation of the odd part exists_contDiff_even_sub_comp_neg_eq_two_mul_smul 1 below · cited by 1 · depth 38
• Common algebraically closed D-algebra receiving two field extensions exists_isAlgClosed_algHom_algHom_of_injective 0 below · cited by 4 · depth 38
• Idempotent–unit splitting for an element coprime to its annihilating factor exists_isIdempotentElem_mul_eq_of_mul_eq_zero_of_isCoprime 0 below · cited by 1 · depth 38
• Symmetry of iterated derivatives within a convex set iteratedFDerivWithin_comp_equivPerm_of_contDiffOn_of_convex 0 below · cited by 2 · depth 40
• Separated-variables product rule on tangential and normal slots iteratedFDeriv_smul_comp_apply_append_inl_inr 0 below · cited by 2 · depth 40