← all areas

Namespace FLT 20 theorems

— 1 · AbstractIntegralStructure 2 · Gamma0FundamentalSet 2 · LedgerRows 1 · ModelTransfer 7 · No2BridgeWiring 2 · OccurrenceStatement 2 · SmoothVectors 3

directly in FLT 1

• Fermat's Last Theorem (Mathlib's formulation) FLT.fermatLastTheorem 29,487 below · cited by 1 · depth 1

FLT.AbstractIntegralStructure 2

• Weight-one χ₋₃ eigensystem occurs mod 3 in weight two FLT.AbstractIntegralStructure.exists_weight_two_eigenform_congruent_of_isLatticeRealized 76 below · cited by 1 · depth 7
• Weight-two eigenform congruent to a mod-3 Hecke eigensystem FLT.AbstractIntegralStructure.exists_weight_two_eigenform_congruent_of_heckeT_congr 74 below · cited by 1 · depth 8

FLT.Gamma0FundamentalSet 2

• Unfolding an integral over a fundamental set into coset integrals FLT.Gamma0FundamentalSet.integral_gammaFundamentalSet_eq_finsum_integral_fd 0 below · cited by 4 · depth 16
• Planar integrals against the smoothed fundamental function FLT.Gamma0FundamentalSet.tendsto_integral_mul_smoothedFundamental 2 below · cited by 4 · depth 20

FLT.LedgerRows 1

• Continuous surjective mod-3 representation with prescribed Frobenius traces FLT.LedgerRows.ledg5_no2_hcurve_continuous 139 below · cited by 2 · depth 8

FLT.ModelTransfer 7

• Model-independence of a_q for q∤ 6 FLT.ModelTransfer.apOfModel_eq_of_isIntegralModelOf 4 below · cited by 1 · depth 9
• Agreement of a_q for models related by a ℚ-change of variables FLT.ModelTransfer.apOfModel_eq_of_isGoodPrimeFor 3 below · cited by 1 · depth 10
• Model-independence of a_q at a common good odd prime FLT.ModelTransfer.apOfModel_eq_of_isIntegralModelOf_odd 3 below · cited by 1 · depth 10
• Point count is invariant under a variable change FLT.ModelTransfer.card_eq_of_variableChange_smul_eq 0 below · cited by 2 · depth 11
• Denominator-clearing data prime to q at a common good prime FLT.ModelTransfer.exists_clearedData_not_dvd 0 below · cited by 1 · depth 11
• Cleared data prime to an odd good prime q FLT.ModelTransfer.exists_clearedData_not_dvd_odd 0 below · cited by 1 · depth 11
• Reduced variable change transfers mod-q reductions FLT.ModelTransfer.reducedChange_smul_reductionMod 0 below · cited by 2 · depth 11

FLT.No2BridgeWiring 2

• Mod-3 eigensystem at a level cube-free away from 3 FLT.No2BridgeWiring.weightOneNewformExists_levelAtThree_not_cube_dvd 7,253 below · cited by 1 · depth 7
• Weight-one χ₋₃ lattice realisation with no cube away from 3 FLT.No2BridgeWiring.weightOneNewformExists_not_cube_dvd 7,221 below · cited by 1 · depth 8

FLT.OccurrenceStatement 2

• Mod-3 Hecke congruence for the weight-one bridge product FLT.OccurrenceStatement.three_dvd_coeff_heckeT_two_sub_smul_of_not_dvd 0 below · cited by 1 · depth 8
• 3 ∣ ℓ - χ₋₃(ℓ) in any commutative ring FLT.OccurrenceStatement.three_dvd_natCast_sub_chiNegThree_cast 0 below · cited by 1 · depth 14

FLT.SmoothVectors 3

• Compactness of the congruence subgroups of GL₂(ℚₚ) FLT.SmoothVectors.isCompact_coe_gl2CongruenceSubgroup 2 below · cited by 1 · depth 15
• Congruence subgroups lie in GL₂(ℤₚ) FLT.SmoothVectors.gl2CongruenceSubgroup_le_integralSubgroup 1 below · cited by 1 · depth 16
• Level-zero congruence subgroup equals GL₂(ℤₚ) FLT.SmoothVectors.gl2CongruenceSubgroup_zero_eq_integralSubgroup 0 below · cited by 1 · depth 17