List view

generalize indexing in lemmas for series

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Merged (completed).

math-comp/analysisnumber 1397

#1397 In math-comp/analysis;

· by t6s was closed on Jan 7, 2025

fixes #1370

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Merged (completed).

math-comp/analysisnumber 1480

#1480 In math-comp/analysis;

· by affeldt-aist was closed on Feb 14, 2025

fixes #1225

Status: Merged (completed).

math-comp/analysisnumber 1475

#1475 In math-comp/analysis;

· by affeldt-aist was closed on Feb 12, 2025

fixes #1471

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Merged (completed).

math-comp/analysisnumber 1472

#1472 In math-comp/analysis;

· by affeldt-aist was closed on Feb 12, 2025

fixes #1468, fixes #1467

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Merged (completed).

math-comp/analysisnumber 1469

#1469 In math-comp/analysis;

· by affeldt-aist was closed on Feb 12, 2025

fixes #1464

documentation 📝This issue/PR is about documentation of the library / repositoryThis issue/PR is about documentation of the library / repository

Status: Merged (completed).

math-comp/analysisnumber 1470

#1470 In math-comp/analysis;

· by affeldt-aist was closed on Feb 18, 2025

fixes #1473

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Merged (completed).

math-comp/analysisnumber 1474

#1474 In math-comp/analysis;

· by affeldt-aist was closed on Feb 12, 2025

minor generalization

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Merged (completed).

math-comp/analysisnumber 1461

#1461 In math-comp/analysis;

· by affeldt-aist was closed on Jan 31, 2025

Pi irrational 20250130

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Merged (completed).

math-comp/analysisnumber 1460

#1460 In math-comp/analysis;

· by affeldt-aist was closed on Jan 31, 2025

l'hopital's rule

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Merged (completed).

math-comp/analysisnumber 1479

#1479 In math-comp/analysis;

· by affeldt-aist was closed on Feb 20, 2025

fixes #1315

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Merged (completed).

math-comp/analysisnumber 1481

#1481 In math-comp/analysis;

· by affeldt-aist was closed on Feb 17, 2025

near lemmas about derivation

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Merged (completed).

math-comp/analysisnumber 1477

#1477 In math-comp/analysis;

· by affeldt-aist was closed on Feb 19, 2025

Pi irrational

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Merged (completed).

math-comp/analysisnumber 1351

#1351 In math-comp/analysis;

· by affeldt-aist was closed on Dec 19, 2024

Accelerated Analysis

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Merged (completed).

math-comp/analysisnumber 1441

#1441 In math-comp/analysis;

· by Tragicus was closed on Dec 21, 2024

minor generalization and renaming

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Merged (completed).

math-comp/analysisnumber 1443

#1443 In math-comp/analysis;

· by affeldt-aist was closed on Dec 29, 2024

Doc: definitions expressed as a table in constructive_ereal.v

documentation 📝This issue/PR is about documentation of the library / repositoryThis issue/PR is about documentation of the library / repository

Status: Merged (completed).

math-comp/analysisnumber 1452

#1452 In math-comp/analysis;

· by yoshihiro503 was closed on Feb 18, 2025

lemma integral_bigsetU_EFin

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Merged (completed).

math-comp/analysisnumber 1447

#1447 In math-comp/analysis;

· by affeldt-aist was closed on Feb 1, 2025

tentative generalization of FTC2

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Merged (completed).

math-comp/analysisnumber 1446

#1446 In math-comp/analysis;

· by affeldt-aist was closed on Feb 18, 2025

monotonous and derivative

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Merged (completed).

math-comp/analysisnumber 1448

#1448 In math-comp/analysis;

· by affeldt-aist was closed on Feb 4, 2025

gen of int. by subst + normal distribution

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Merged (completed).

math-comp/analysisnumber 1450

#1450 In math-comp/analysis;

· by affeldt-aist was closed on Feb 19, 2025

nondecreasing functions have a countable number of discontinuities

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Merged (completed).

math-comp/analysisnumber 1451

#1451 In math-comp/analysis;

· by affeldt-aist was closed on Feb 5, 2025

differentiation under integral

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Merged (completed).

math-comp/analysisnumber 1435

#1435 In math-comp/analysis;

· by affeldt-aist was closed on Feb 6, 2025

split lebesgue_measure.v

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Closed (completed).

#1315 In math-comp/analysis;

· by affeldt-aist was closed on Feb 17, 2025

document near do

documentation 📝This issue/PR is about documentation of the library / repositoryThis issue/PR is about documentation of the library / repository

Status: Closed (completed).

#1395 In math-comp/analysis;

· by affeldt-aist was closed on Feb 18, 2025

renaming Rintegral_setU_EFin

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Closed (completed).

#1370 In math-comp/analysis;

· by affeldt-aist was closed on Feb 14, 2025