Issues

• Use a sensible sort order in multiset.repr

  leanprover-community/mathlib3#18166 · Filter by author eric-wieser opened on Jan 13, 2023

• Tracking: attribute semireducible/irreducible

  mathportneeds-refactor
  leanprover-community/mathlib3#18164 · Filter by author jcommelin opened on Jan 13, 2023

• (a :: l ++ [b]).last' does not simplify to some b

  leanprover-community/mathlib3#18010 · Filter by author jcpaik opened on Dec 24, 2022

• polyrith fails if expression is an equality of numerals

  bugt-meta
  leanprover-community/mathlib3#17141 · Filter by author eric-wieser opened on Oct 24, 2022

• Diamond of complete boolean algebras on sets

  leanprover-community/mathlib3#16932 · Filter by author ocfnash opened on Oct 12, 2022

• Basics of tempered distributions

  long termt-analysis
  leanprover-community/mathlib3#16386 · Filter by author mcdoll opened on Sep 5, 2022
  1

• evaluate int.floor and int.fract with norm_num

  feature-request
  leanprover-community/mathlib3#15992 · Filter by author vihdzp opened on Aug 10, 2022
  2

• Refactor bilinear forms

  RFCt-algebra
  leanprover-community/mathlib3#15907 · Filter by author mcdoll opened on Aug 7, 2022

• Pi is irrational

  good-first-projectt-analysis
  leanprover-community/mathlib3#15860 · Filter by author mcdoll opened on Aug 4, 2022
  5

• Cleanup direct_sum.sigma_curry / direct_sum.is_internal.collected_basis

  t-algebra
  leanprover-community/mathlib3#15756 · Filter by author ADedecker opened on Jul 29, 2022

• Remove has_coe_to_fun instance for unitary_group

  good-first-project
  leanprover-community/mathlib3#15749 · Filter by author mcdoll opened on Jul 29, 2022

• Banach-Alaoglu for topological vector spaces

  feature-request
  leanprover-community/mathlib3#15734 · Filter by author mcdoll opened on Jul 28, 2022

• expand_exists improvements

  t-meta
  leanprover-community/mathlib3#15723 · Filter by author robertylewis opened on Jul 27, 2022
  1

• Locally convex Hausdorff spaces

  feature-requestgood-first-project
  leanprover-community/mathlib3#15565 · Filter by author mcdoll opened on Jul 20, 2022

• Add an instance {add_,}sub{monoid,group}_class S M → has_coe_t S ({add_,}sub{monoid,group} M)

  leanprover-community/mathlib3#15053 · Filter by author Vierkantor opened on Jun 29, 2022

• nth_rewrite incorrectly unifies universe variables

  bugt-meta
  leanprover-community/mathlib3#14994 · Filter by author fpvandoorn opened on Jun 27, 2022

• apply' can close the goal with metavariables

  bugt-meta
  leanprover-community/mathlib3#14993 · Filter by author fpvandoorn opened on Jun 27, 2022

• Approximation tactic

  feature-request
  leanprover-community/mathlib3#14781 · Filter by author BoltonBailey opened on Jun 16, 2022
  1

• Create library note explaining seemingly redundant fintype and decidable arguments.

  leanprover-community/mathlib3#14275 · Filter by author kmill opened on May 20, 2022
  1

• padic_norm file maintenance

  leanprover-community/mathlib3#13574 · Filter by author BoltonBailey opened on Apr 21, 2022

• convert is_monoid_hom etc to structures, and move out of deprecated

  leanprover-community/mathlib3#13506 · Filter by author kim-em opened on Apr 19, 2022

• to_ framework

  feature-requestt-meta
  leanprover-community/mathlib3#13461 · Filter by author YaelDillies opened on Apr 15, 2022
  1

• let linear_combination solve ≠ goals

  feature-requestmodifies-tactic-syntaxt-meta
  leanprover-community/mathlib3#12685 · Filter by author hrmacbeth opened on Mar 14, 2022

• Lipschitz embeddings into ℓ^∞

  good-first-project
  leanprover-community/mathlib3#11571 · Filter by author hrmacbeth opened on Jan 20, 2022

• Arithmetic of quadratic fields

  feature-request
  leanprover-community/mathlib3#11407 · Filter by author riccardobrasca opened on Jan 12, 2022
  6