Home

formathlib PR status

Check status using git ls-files | grep for_mathlib | xargs wc -l from the repository root.

• Gordan.lean
• Profinite/functorial_limit.lean
• Profinite/locally_constant.lean
• Profinite/nhds.lean
• Top/limits.lean -- #7448
• arrow.lean -- PR exists
• dfinsupp.lean
• equalizers.lean
• finsupp.lean
• free_abelian_group.lean
• grading.lean
• grading_examples.lean
• grading_monoid_algebra.lean
• grading_zero_subring.lean
• int_grading_lemma.lean
• kronecker.lean
• linear_algebra.lean
• pseudo_metric.lean
• SemiNormedGroup_Completion.lean -- #9788
• simplicial/complex.lean
• specific_limit.lean
• tsum.lean
• SemiNormedGroup.lean -- #9710 #9711 and #9712
• normed_group.lean -- Patrick will work on it once #7528 lands
• normed_group_hom.lean
• normed_group_hom_completion.lean
• normed_group_hom_equalizer.lean -- #8228
• normed_group_quotient.lean --RB and PM working on it
• simplicial/augmented.lean -- PR #7614
• nnreal.lean -- PR #7471
• preadditive_category.lean -- PR 7533
• Profinite.lean -- PR #7529
• normed_group_hom.lean --PR #7459, #7468 and #7474
• data_set_lattice.lean -- PR #7557
• curry.lean -- PR #7458
• order_basic.lean -- PR 7469
• Fintype/basic.lean -- PR #7491
• Profinite/limits.lean -- PR #7448
• uniform_space_cauchy.lean -- PR #7528
• pi_nat_apply.lean -- PR 7492
• real_Inf.lean --PR #7524. NB: some names are different and we use 0 < ε
• filter_at_top_bot.lean -- PR 7469
• category.lean -- PR exists
• big_operators_basic.lean -- PR #7470
• quotient_group.lean --PR #7523 mk'_eq_mk'_iff has become quotient_add_group.eq_iff_sub_mem and it uses ↑ instead of mk'