Home

formathlib PR status

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

• Fintype/basic.lean -- PR #7491
• Gordan.lean
• Profinite.lean -- PR #7529
• Profinite/functorial_limit.lean
• Profinite/limits.lean -- PR #7448
• Profinite/locally_constant.lean
• Profinite/nhds.lean
• Top/limits.lean -- #7448
• arrow.lean -- PR exists
• curry.lean -- PR #7458
• data_set_lattice.lean -- PR #7557
• 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
• nnreal.lean -- PR #7471
• normed_group.lean -- Patrick will work on it once #7528 lands
• normed_group_hom.lean --PR #7459, #7468 and #7474
• normed_group_hom_bound_by.lean
• normed_group_hom_completion.lean
• normed_group_hom_equalizer.lean
• normed_group_quotient.lean --RB and PM working on it
• order_basic.lean -- PR 7469
• preadditive_category.lean -- PR 7533
• pseudo_metric.lean
• quotient_group.lean --PR #7523 mk'_eq_mk'_iff has become quotient_add_group.eq_iff_sub_mem and it uses ↑ instead of mk'
• simplicial/augmented.lean
• simplicial/complex.lean
• specific_limit.lean
• tsum.lean
• 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