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
• 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
• 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 working on it
• order_basic.lean -- PR 7469
• pi_nat_apply.lean -- PR 7492
• preadditive_category.lean -- PR 7533
• pseudo_metric.lean
• quotient_group.lean --PR #7523 mk'_eq_mk'_iff has become quotient_add_group.eq_of_normal
• real_Inf.lean --PR #7524. NB: some names are different and we use 0 < ε
• simplicial/augmented.lean
• simplicial/complex.lean
• specific_limit.lean
• tsum.lean
• uniform_space_cauchy.lean -- PR #7528
• filter_at_top_bot.lean -- PR 7469
• category.lean -- PR exists
• big_operators_basic.lean -- PR #7470