Skip to content

mv charge to measure and lebesgue_integral#1953

Open
affeldt-aist wants to merge 1 commit intomath-comp:masterfrom
affeldt-aist:charge_20260426
Open

mv charge to measure and lebesgue_integral#1953
affeldt-aist wants to merge 1 commit intomath-comp:masterfrom
affeldt-aist:charge_20260426

Conversation

@affeldt-aist
Copy link
Copy Markdown
Member

@affeldt-aist affeldt-aist commented Apr 26, 2026

Motivation for this change

This PR splits the file charge.v into a measure-only part
(signed_measure.v) and a part depending on the Lebesgue integral
(radon_nikodym.v), so that we have one less file at the root.

@IshiguroYoshihiro can you check this PR?

Checklist
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

  • PRs with several commits that make sense individually and that
    all compile are preferentially merged into master.
  • PRs with disorganized commits are very likely to be squash-rebased.
Reminder to reviewers

@affeldt-aist affeldt-aist requested a review from mkerjean April 26, 2026 08:07
@affeldt-aist affeldt-aist added this to the 1.17.0 milestone Apr 26, 2026
@affeldt-aist affeldt-aist added the renaming/refactoring 🔧 This is about a renaming or refactoring in the library label Apr 26, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

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

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant