leanprover-community / mathlib4

The math library of Lean 4

Apache License 2.0

1.37k stars 307 forks source link

Open Ruben-VandeVelde opened 1 year ago

Ruben-VandeVelde commented 1 year ago

The following extensions are still missing:

[ ] EReal (Mathlib/Data/Real/EReal.lean)
[ ] powers on ℝ≥0 and ℝ≥0∞ (Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean)
[x] Finset.card (Mathlib/Data/Fintype/Card.lean)
[ ] • (Algebra.Order.SMul)
[x] Real.sqrt/NNReal.sqrt (Data.Real.Sqrt). There are two extensions, but they are currently broken
[ ] ... probably more

YaelDillies commented 4 months ago

3907 did `Real.sqrt`/`NNReal.sqrt`, #10610 did `Finset.card`.