Search results

Use a sensible sort order in multiset.repr

Status: Open.

#18166 In leanprover-community/mathlib3;

· eric-wieser opened on Jan 13, 2023

Tracking: attribute semireducible/irreducible

mathportFor compatibility with Lean 4 changes, to simplify portingFor compatibility with Lean 4 changes, to simplify porting

needs-refactor

Status: Open.

#18164 In leanprover-community/mathlib3;

· jcommelin opened on Jan 13, 2023

<code>(a :: l ++ [b]).last'</code> does not simplify to <code>some b</code>

Status: Open.

#18010 In leanprover-community/mathlib3;

· jcpaik opened on Dec 24, 2022

<code>polyrith</code> fails if expression is an equality of numerals

bug

t-metaTactics, attributes or user commandsTactics, attributes or user commands

Status: Open.

#17141 In leanprover-community/mathlib3;

· eric-wieser opened on Oct 24, 2022

Diamond of complete boolean algebras on sets

Status: Open.

#16932 In leanprover-community/mathlib3;

· ocfnash opened on Oct 12, 2022

Basics of tempered distributions

long term

t-analysisAnalysis (normed *, calculus)Analysis (normed *, calculus)

Status: Open.

#16386 In leanprover-community/mathlib3;

· mcdoll opened on Sep 5, 2022

evaluate <code>int.floor</code> and <code>int.fract</code> with <code>norm_num</code>

feature-requestThis issue is a feature request, either for mathematics, tactics, or CIThis issue is a feature request, either for mathematics, tactics, or CI

Status: Open.

#15992 In leanprover-community/mathlib3;

· vihdzp opened on Aug 10, 2022

Refactor bilinear forms

RFCRequest for commentRequest for comment

t-algebraAlgebra (groups, rings, fields etc)Algebra (groups, rings, fields etc)

Status: Open.

#15907 In leanprover-community/mathlib3;

· mcdoll opened on Aug 7, 2022

Pi is irrational

good-first-project

t-analysisAnalysis (normed *, calculus)Analysis (normed *, calculus)

Status: Open.

#15860 In leanprover-community/mathlib3;

· mcdoll opened on Aug 4, 2022

Cleanup <code>direct_sum.sigma_curry</code> / <code>direct_sum.is_internal.collected_basis</code>

t-algebraAlgebra (groups, rings, fields etc)Algebra (groups, rings, fields etc)

Status: Open.

#15756 In leanprover-community/mathlib3;

· ADedecker opened on Jul 29, 2022

Remove <code>has_coe_to_fun</code> instance for <code>unitary_group</code>

good-first-project

Status: Open.

#15749 In leanprover-community/mathlib3;

· mcdoll opened on Jul 29, 2022

Banach-Alaoglu for topological vector spaces

feature-requestThis issue is a feature request, either for mathematics, tactics, or CIThis issue is a feature request, either for mathematics, tactics, or CI

Status: Open.

#15734 In leanprover-community/mathlib3;

· mcdoll opened on Jul 28, 2022