Skip to content

measurable bigmax - #2092

Open
affeldt-aist wants to merge 1 commit into
math-comp:masterfrom
affeldt-aist:measurable_20260823
Open

measurable bigmax#2092
affeldt-aist wants to merge 1 commit into
math-comp:masterfrom
affeldt-aist:measurable_20260823

Conversation

@affeldt-aist

Copy link
Copy Markdown
Member
Motivation for this change

Easy lemma about measurability and bigmax used to reason about the matrix norm.

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 added this to the 1.18.0 milestone Aug 23, 2026
@affeldt-aist affeldt-aist added the enhancement ✨ This issue/PR is about adding new features enhancing the library label Aug 23, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

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

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant