Skip to content

corollary to Vitali's theorem#1328

Merged
affeldt-aist merged 4 commits intomath-comp:masterfrom
affeldt-aist:vitali_corollary
Oct 8, 2024
Merged

corollary to Vitali's theorem#1328
affeldt-aist merged 4 commits intomath-comp:masterfrom
affeldt-aist:vitali_corollary

Conversation

@affeldt-aist
Copy link
Member

@affeldt-aist affeldt-aist commented Sep 26, 2024

Motivation for this change

also fixes #1334

Checklist
  • added corresponding entries in CHANGELOG_UNRELEASED.md

- [ ] added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

@affeldt-aist affeldt-aist added the enhancement ✨ This issue/PR is about adding new features enhancing the library label Sep 26, 2024
@affeldt-aist affeldt-aist added this to the 1.5.0 milestone Sep 26, 2024
@affeldt-aist affeldt-aist merged commit 9033e92 into math-comp:master Oct 8, 2024
@affeldt-aist affeldt-aist deleted the vitali_corollary branch October 8, 2024 09:01
IshiguroYoshihiro pushed a commit to IshiguroYoshihiro/analysis that referenced this pull request Oct 9, 2024
* corollary to Vitali's theorem

* fixes math-comp#1334

* rm deprecated
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.

move Require Import to top of the file

2 participants