File Churn · anthropics/fermats-last-theorem

Overview

File Change Frequency Overall

There are 0 files with 0 lines of code.

0 files changed more than 100 times (0 lines of code)
0 files changed 51-100 times (0 lines of code)
0 files changed 21-50 times (0 lines of code)
0 files changed 6-20 times (0 lines of code)
0 files changed 1-5 times (0 lines of code)

Legend:

101+

51-100

21-50

6-20

1-5

explore: grouped by folders | grouped by update frequency | data

Contributors Count Frequency Overall

There are 0 files with 0 lines of code.

0 files changed by more than 25 contributors (0 lines of code)
0 files changed by 11-25 contributors (0 lines of code)
0 files changed by 6-10 contributors (0 lines of code)
0 files changed by 2-5 contributors (0 lines of code)
0 files changed by 1 contributor (0 lines of code)

Legend:

26+

11-25

6-10

2-5

explore: grouped by folders | grouped by contributors count | data

File Change Frequency per File Extension

lean, html, js, txt, py, md, json, css, diff, sh, svg, gitignore, gitattributes, toml, yaml

File Change Frequency per Extension

The number of recorded file updates

101+

51-100

21-50

6-20

1-5

File Change Frequency per Logical Decomposition

primary

primary (file change frequency)

The number of recorded file updates

101+

51-100

21-50

6-20

1-5

Most Frequently Changed Files (Top 50)

See data for all files...

File	# lines	# units
lean D_AutomorphicForm_ArchDirComplex_DecidableEq.lean in P2M/Derive	2	-
lean S_GaloisRepAdic_det_residual.lean in P2M/Sol	4	-
lean Thm_CuspForm_heckeLocal_residue_surjective.lean in Theorems	4	-
lean Thm_Module_Finite_of_ker_le_range_of_isNoetherianRing.lean in Theorems	4	-
lean Thm_ModularCurve_sharpUnitNecessary_of_mod_oneTwenty_eq_one_or_fortyNine.lean in Theorems	4	-
lean Thm_rademacher_phi_level_witness_mod_sixty_eq_thirteen.lean in Theorems	4	-
lean Thm_AlgebraicCurve_Place_exists_toValuationSubring_eq_comap_ringHom.lean in Theorems	4	-
lean Thm_FrobeniusEndo_exists_prime_gt_and_quadratic_root.lean in Theorems	4	-
lean Thm_WeierstrassCurve_Affine_FunctionField_exists_eq_algebraMap_of_valuation_eq_one.lean in Theorems	4	-
lean Thm_GaloisRepAdic_trace_baseChangeAlong.lean in Theorems	4	-
lean Thm_WeierstrassCurve_Psi2Sq_ne_zero_of_isElliptic.lean in Theorems	4	-
lean Thm_exists_intCast_eq_six_mul_dedekindSum.lean in Theorems	4	-
lean Thm_ModularCurve_isMonicOfOrder_sharpUnitSeries.lean in Theorems	4	-
lean Thm_Polynomial_exists_root_reducing_to_simple_root.lean in Theorems	4	-
lean Thm_dedekindSum_natCast_sub_one.lean in Theorems	4	-
lean Thm_MonoidHom_charpoly_apply_mul_mul_inv.lean in Theorems	4	-
lean Thm_ModularCurve_exists_perm_gamma0_cosetReps.lean in Theorems	4	-
lean Thm_RatFunc_exists_algEquiv_apply_X_eq_moebius.lean in Theorems	4	-
lean Thm_WeierstrassCurve_Affine_FunctionField_adjoin_X_Y_eq_top.lean in Theorems	4	-
lean Thm_CongruenceSubgroup_one_mem_strictPeriods_Gamma0.lean in Theorems	4	-
lean Thm_WeierstrassCurve_exists_powerSeries_isElliptic_variableChange_smul_map_eq_and_map_j_ne_C.lean in Theorems	4	-
lean Thm_ModularCurve_laurentBaseChange_mono.lean in Theorems	4	-
lean Thm_LaurentSeries_eq_C_coeff_zero_of_isAlgebraic.lean in Theorems	4	-
lean Thm_ModularCurve_smulCommClass_JZero_of_heckeOperatorsCommuteBar.lean in Theorems	4	-
lean Thm_ValuationSubring_exists_pow_prime_pow_eq_self_of_isAlgebraic.lean in Theorems	4	-
lean Thm_WeierstrassCurve_finite_stabilizer_variableChange.lean in Theorems	4	-
lean Thm_ModularCurve_exists_hauptmodulFive_of_kernelQuadratic.lean in Theorems	4	-
lean Thm_GaloisRepAdic_det_residual.lean in Theorems	4	-
lean Thm_ModularCurve_qExpansionDiffAlong_smul.lean in Theorems	4	-
lean Thm_AlgHom_natCard_eq_finrank_of_isReduced_of_isAlgClosed.lean in Theorems	4	-
lean Thm_AlgebraicCurve_Place_exists_of_valuationSubring.lean in Theorems	4	-
lean Thm_IsReduced_of_finrank_le_natCard_algHom.lean in Theorems	4	-
lean Thm_NumberField_exists_lift_mem_inertia_integralClosure.lean in Theorems	4	-
lean Thm_dedekindSum_add_dedekindSum.lean in Theorems	4	-
lean Thm_AlgebraicCurve_isTraceDiff_traceDiff.lean in Theorems	4	-
lean Thm_ModularCurve_qExpansionDiffAlong_smul_map.lean in Theorems	4	-
lean Thm_ModularCurve_qExpansionDiffAlong_smul_map_D.lean in Theorems	4	-
lean Thm_AlgebraicCurve_traceDiff_inv_smul_D_eq_inv_norm_smul_D_norm.lean in Theorems	4	-
lean Thm_IntermediateField_finrank_fieldRange_le_of_adjoin_pair_eq_top.lean in Theorems	4	-
lean Thm_Int_exists_not_dvd_and_le_and_not_isSquare_and_forall_prime_of_sq_sub_four_mul_ne_zero.lean in Theorems	4	-
lean Thm_IsDedekindDomain_HeightOneSpectrum_exists_eq_span_singleton_of_map_eq.lean in Theorems	4	-
lean Thm_AlgebraicCurve_traceDiff_apply.lean in Theorems	4	-
lean Thm_ModularCurve_coeffEmb_injective.lean in Theorems	4	-
lean Thm_Polynomial_mem_range_of_eval_eq_const.lean in Theorems	4	-
lean Thm_WeierstrassCurve_Affine_FunctionField_exists_valuation_eq_exp_natDegree_norm.lean in Theorems	4	-
lean Thm_CuspForm_HeckeGaloisRepDatum_surjective_of_isEquiv_baseChangeAlong.lean in Theorems	4	-
lean Thm_AlgebraicCurve_FunctionField_exists_ratFuncAlgHom_apply_X_eq.lean in Theorems	4	-
lean Thm_ModularForm_eta_add_intCast.lean in Theorems	4	-
lean Thm_rademacher_phi_level_witness_mod_oneTwenty_eq_one.lean in Theorems	4	-
lean Thm_WeierstrassCurve_exists_variableChange_map_subtype_eq_and_smul_eq_of_isUnit_discriminant.lean in Theorems	4	-

Files With Most Contributors (Top 50)

Based on the number of unique email addresses found in commits.

See data for all files...

File	# lines	# units
katex_render.js in tools/docs-site/gen	16	-
graphdata.py in tools/docs-site/gen	183	3
build.py in tools/docs-site/gen	41	1
selfcheck.py in tools/docs-site/gen	155	2
render.py in tools/docs-site/gen	1059	21
qa_filetest.py in tools/docs-site/gen	85	4
site.css in tools/docs-site/gen/assets	144	-
site.js in tools/docs-site/gen/assets	358	27
explorer.js in tools/docs-site/gen/assets	153	7
hl.js in tools/docs-site/gen/assets	55	2
extract.py in tools/docs-site/gen	163	2
lean Thm_Rep_tateDelta_splitting_tateDelta_aug_eq_map_H2pi.lean in Theorems	18	-
lean Thm_Algebra_FormallyUnramified_algEquiv_apply_eq_of_mem_inertiaSubgroupIn_padicIntegers.lean in Theorems	13	-
lean Thm_HeckeEis_IsEichlerIntegral_vadd_sub_T_zpow_apply_mem_range.lean in Theorems	14	-
lean Thm_ModularCurve_JHNeronObjectAtP_smul_eq_nsmul_of_mem_toricPts_of_mem_inertiaSubgroupIn.lean in Theorems	17	-
lean Thm_CerednikDrinfeld_QM_FakeEllipticCurve_IsFormalModuleOf_isSpecial.lean in Theorems	13	-
lean Thm_IsLocalRing_herbrandPhi_eq_herbrandPhi_quotient_comp_of_map_lowerRamificationGroup_mk_eq.lean in Theorems	17	-
lean Thm_GoodReductionJacobian_RelativeGroupLaw_dualNumber_eq_comp_of_ker_ribetMatrix.lean in Theorems	42	-
lean Thm_CerednikDrinfeld_Omega_exists_isUnit_coe_eq_thetaMer_apply_smul_eq_period_mul.lean in Theorems	20	-
lean Thm_ModularCurve_FullLevel_AuxLevelOne_exists_blowupChart_ringHom_coordRing_surjective_ker_eq_span_of_chartMap_of_localFibreMap_of_dvd.lean in Theorems	134	-
lean Thm_AlgebraicGeometry_Scheme_Modules_ProjPresentation_locallyQuasiFinite_of_forall_exists_eq_sum_smul.lean in Theorems	13	-
lean Thm_CerednikDrinfeld_QM_IsFineModuliT_exists_apply_ne_zero_forall_isPullback_of_cerednikDrinfeld_uniformization_fine_eq.lean in Theorems	143	-
lean Thm_IntermediateField_IsUnramifiedOutside_sup_adjoin_simple_of_pow_mem.lean in Theorems	12	-
lean Thm_QuaternionAlgebra_exists_nrd_eq_of_pos_of_isDefiniteRamifiedExactlyAt.lean in Theorems	13	-
lean Thm_PowerSeries_norm_tsum_coeff_mul_pow_le_mul_prod.lean in Theorems	12	-
lean Thm_ValuationSubring_exists_subfield_henselian_isDiscreteValuationRing_inf_of_liesOverPrime.lean in Theorems	21	-
lean Thm_ModularCurve_ModularPolynomialData_map_map_intCast_eq_of_charP.lean in Theorems	12	-
lean Thm_AlgebraicGeometry_ProjSpace_exists_affSES_twist_succ_of_forall_mul_eq_zero_imp.lean in Theorems	76	-
lean Thm_LanglandsTunnell_CubicInduction_isGL3PsiWhittakerFn_of_forall_isGL3PsiWhittakerFn_finsum_cpow_mul.lean in Theorems	14	-
lean Thm_AlgHom_range_eq_range_aeval_X_of_isIntegral_adjoin_singleton.lean in Theorems	12	-
lean Thm_ModularCurve_UVCrossingModel_exists_ringEquiv_quotient_span_U_powerSeries.lean in Theorems	6	-
lean Thm_ModularCurve_exists_mem_periodLattice_eq_sum_intCast_mul_edgeIntegral_of_isParabolicHom.lean in Theorems	30	-
lean Thm_AlgebraicCurve_sum_absLogHeight_roots_le_coeff.lean in Theorems	9	-
lean Thm_CerednikDrinfeld_Omega_semilinearAut_smul_pt_eq_pt_smul_of_mem_toValuationSubring_iff.lean in Theorems	30	-
lean Thm_AlgebraicCurve_genus_eq_of_constantFieldExtension_of_isAlgClosed.lean in Theorems	20	-
lean Thm_ModularCurve_coeff_cuspPoint_fst_add_inv_twelve_sq_of_ne_zero.lean in Theorems	16	-
lean Thm_IsOpen_exists_numberField_ker_restrictNormalHom_le.lean in Theorems	9	-
lean Thm_AlgebraicGeometry_Scheme_IdealSheafData_comap_ofIdealTop.lean in Theorems	10	-
lean Thm_AutomorphicForm_isKfSmooth_unipotentAverage.lean in Theorems	17	-
lean Thm_GoodReductionJacobian_RelativeGroupLaw_smoothOfRelativeDimension_of_forall_topologicalKrullDim_eq.lean in Theorems	13	-
lean Thm_CerednikDrinfeld_QM_forall_trace_eq_intCast_of_isFormalCoordinates_of_isSpecial.lean in Theorems	31	-
lean Thm_Module_rankAtStalk_eq_of_forall_localizedModule_equiv.lean in Theorems	14	-
lean Thm_ModularCurve_IgusaScheme_isProper_igusaTo.lean in Theorems	9	-
lean Thm_AlgebraicGeometry_Scheme_fppfKummerRow_naturality.lean in Theorems	22	-
lean Thm_ModularCurve_monic_fibrePoly.lean in Theorems	9	-
lean Thm_LT_LatticeTree_Vertex_isWithin_iff_dist_le.lean in Theorems	11	-
lean Thm_ModularCurve_UVCrossingModel_leadingResidue_nfCoeff_eq_residue_constantCoeff_and_mem_dominantIndices_of_sub_mul_U_pow_mem.lean in Theorems	18	-
lean Thm_ModularCurve_DRModelPackage_mem_preimage_and_forall_evalAt_eq_stalkClosedPointTo_of_ord_sub_pos.lean in Theorems	90	-
lean Thm_Matrix_exists_det_eq_one_unipotent_forall_mul_mem_of_not_le_of_not_le.lean in Theorems	10	-
lean Thm_NumberField_InfinitePlace_isUnramifiedIn_of_pow_eq.lean in Theorems	11	-

Files With Least Contributors (Top 50)

Based on the number of unique email addresses found in commits.

See data for all files...

File	# lines	# units
lean S_AutomorphicForm_exists_forall_lintegral_norm_sq_deriv_normalizedIntertwining_axis_le_of_completedL_mul_weylIntertwiningIntegral_eq_of_flat.lean in P2M/Sol	8429	-
lean S_LocalNewvector_PSCarrier_finrank_inf_fixedSubmodule_padicK1_of_stable.lean in P2M/Sol	7751	-
lean S_LocalNewvector_PSCarrier_existsUnique_mem_inf_fixedSubmodule_padicK1_one_of_stable.lean in P2M/Sol	7747	-
lean S_Ihara_mennickeCSP_of_prime.lean in P2M/Sol	7680	-
lean S_UnipotentTermCuspBound_exists_forall_setLIntegral_tsum_setLIntegral_enorm_mul_tsum_tsum_enorm_sub_ne_top.lean in P2M/Sol	6800	-
lean S_QuadraticForm_exists_rat_ternary_pureNrd_eq_of_forall_adicCompletion_of_real.lean in P2M/Sol	6794	-
lean S_QuadraticForm_forall_exists_ternary_pureNrd_eq_of_exists_ne_zero_eq_zero.lean in P2M/Sol	6771	-
lean S_NumberField_TateGlobal_zetaIntegral_meromorphic_continuation_fe.lean in P2M/Sol	6511	-
lean S_ModularCurve_PDPairing_pairZFun_jDeg0_iDeg0.lean in P2M/Sol	6438	-
lean S_ModularCurve_PDPairing_pairZFun_heckeT0_comm.lean in P2M/Sol	6437	-
lean S_ModularCurve_PDPairing_isFreeGroup_Gamma_four.lean in P2M/Sol	6435	-
lean S_ModularCurve_PDPairing_index_Gamma_four.lean in P2M/Sol	6434	-
lean S_LanglandsTunnell_Converse_exists_archDatumC_W_ne_zero.lean in P2M/Sol	6313	-
lean S_LanglandsTunnell_Converse_ArchDatumC_norm_iteratedFDerivWithin_diagOne_le.lean in P2M/Sol	6235	-
lean S_LanglandsTunnell_Converse_ArchDatumC_exists_W_eq_fderivWithin_mul.lean in P2M/Sol	6231	-
lean S_AutomorphicForm_exists_analyticOnNhd_normalizedIntertwining_completedL_mul_axis_continuation_weylIntertwiningIntegral_eq_mul_of_flat.lean in P2M/Sol	6211	-
lean S_AutomorphicForm_exists_analyticOnNhd_continuousOn_normalisedIntertwining_of_isInducedSection_family.lean in P2M/Sol	6066	-
lean S_AutomorphicForm_GL2Twisted_twistedOrbitalIntegral_eq_twistedSplitTransform_div_and_eq_twistedEllipticTransform_div.lean in P2M/Sol	6021	-
lean S_LanglandsTunnell_CubicInduction_exists_contDiff_hasCompactSupport_eq_integral_archRealLift3.lean in P2M/Sol	5837	-
lean S_AutomorphicForm_semilocal_central_transfer_referenceMeasures_peel_step.lean in P2M/Sol	5695	-
lean S_LocalNewvector_PSCarrier_isIrreducibleGLRep_of_hasCharConductor_of_ratio.lean in P2M/Sol	5618	-
lean S_NumberField_TateGlobal_exists_differentiable_eq_partialEulerProduct_of_exists_mem_normOneIdeles_ne_one.lean in P2M/Sol	5449	-
lean S_NumberField_TateGlobal_exists_meromorphicOn_eq_partialEulerProduct.lean in P2M/Sol	5396	-
lean S_NumberField_TateGlobal_exists_meromorphicOn_analyticAt_one_eq_partialEulerProduct_of_ne_one.lean in P2M/Sol	5367	-
lean S_LanglandsTunnell_Converse_PrincipalFamily_isCasimirEigen_of_W_eq_comb.lean in P2M/Sol	5306	-
lean S_LanglandsTunnell_Converse_PrincipalFamily_oddComb_archWeightChar.lean in P2M/Sol	5211	-
lean S_NumberField_TateGlobal_integrable_zetaIntegrand.lean in P2M/Sol	5200	-
lean S_AutomorphicForm_exists_nhds_forall_exists_isLocalTestFn_areMatchingLocal_of_isRegularSemisimple_normString.lean in P2M/Sol	5198	-
lean S_LocalNewvector_PSCarrier_fixedSubmodule_padicK1_zero_le_of_stable.lean in P2M/Sol	5191	-
lean S_LanglandsTunnell_Converse_PrincipalFamily_exists_oddComb_ne_zero.lean in P2M/Sol	5149	-
lean S_AutomorphicForm_twistedOrbitalIntegral_eq_shadow_of_irreducible_charpoly.lean in P2M/Sol	5117	-
lean S_LanglandsTunnell_Converse_ArchDatumR_norm_iteratedFDerivWithin_diagOne_le.lean in P2M/Sol	5016	-
lean S_LanglandsTunnell_Converse_ArchDatumR_exists_W_eq_fderivWithin_mul.lean in P2M/Sol	5013	-
lean S_AutomorphicForm_TransversalMeasure_exists_forall_lintegral_eq_lintegral_mul_prod_of_forall_prod_archSemiLocalIdele.lean in P2M/Sol	4799	-
lean S_NumberField_TateGlobal_exists_forall_zetaIntegral_mul_eulerFactors_eq_of_eq_indicator.lean in P2M/Sol	4698	-
lean S_NumberField_TateGlobal_zetaIntegral_mul_eulerFactors_eq.lean in P2M/Sol	4687	-
lean S_TwistedUnipotentTerm_exists_transversal.lean in P2M/Sol	4631	-
lean S_AlgebraicGeometry_nonempty_towerQuotientDatum_of_isProper_of_flat_of_forall_exists_isAffineOpen.lean in P2M/Sol	4519	-
lean S_LanglandsTunnell_Converse_PrincipalFamily_exists_archDatumR_W_eq.lean in P2M/Sol	4510	-
lean S_LanglandsTunnell_Converse_exists_archDatumR_principal_W_ne_zero.lean in P2M/Sol	4505	-
lean S_LanglandsTunnell_Converse_PrincipalFamily_exists_Wmem_ne_zero.lean in P2M/Sol	4490	-
lean S_AutomorphicForm_semilocal_central_transfer_peel_step.lean in P2M/Sol	4442	-
lean S_LanglandsTunnell_CubicInduction_AdelicEpstein_exists_forall_epstein_eq_div_sub_one_add_of_pureTensor.lean in P2M/Sol	4432	-
lean S_ModularCurve_UVCrossingModel_exists_mul_length_eq_mul_finrank_of_ne_bot_of_const_notMem.lean in P2M/Sol	4371	-
lean S_LanglandsTunnell_CubicInduction_jacquetVector3_isArchZetaConvergentAbove.lean in P2M/Sol	4334	-
lean S_LocalNewvector_PSCarrier_isIrreducibleGLRep_of_isUnramified.lean in P2M/Sol	4216	-
lean S_ModularCurve_UVCrossingModel_moduleFinite_quotient_of_not_le_span_pair.lean in P2M/Sol	4165	-
lean S_RegularSingular_exists_norm_apply_le_const_mul_one_add_pow_mul_rpow.lean in P2M/Sol	4134	-
lean S_LanglandsTunnell_CubicInduction_integrable_dualWhittakerFn3_jacquetVector3_prod.lean in P2M/Sol	4133	-
lean Def_ModularCurve_SpecializationMap.lean in Definitions	4091	-

Correlations

File Size vs. Number of Changes: 0 points

No data for "lines of code" vs. "# changes".

Number of Contributors vs. Number of Changes: 0 points

No data for "# contributors" vs. "# changes".

Number of Contributors vs. File Size: 0 points

No data for "# contributors" vs. "lines of code".

Number of Changes vs. Line Churn: 1 points

		4.0	line churn min: 4.0 average: 4.0 25th percentile: 4.0 median: 4.0 75th percentile: 4.0 max: 4.0
0	2.0
# changes min: 2.0 \| average: 2.0 \| 25th percentile: 2.0 \| median: 2.0 \| 75th percentile: 2.0 \| max: 2.0

Number of Contributors vs. Line Churn: 0 points

No data for "# contributors" vs. "line churn".

File Size vs. Line Churn: 0 points

No data for "lines of code" vs. "line churn".