[Merged by Bors] - feat: the non-unital star subalgebra generated by id is dense in C(s, 𝕜)₀
#13326
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
j-loreaux
added
awaiting-review
j-loreaux
changed the base branch from
j-loreaux/ContinuousMapZeroMaterial
to
master
dupuisf
reviewed
May 29, 2024
Comment on lines
+6
to
10
| import Mathlib.Algebra.Algebra.Subalgebra.Unitization | ||
| import Mathlib.Analysis.RCLike.Basic | ||
| import Mathlib.Topology.Algebra.StarSubalgebra | ||
| import Mathlib.Topology.ContinuousFunction.ContinuousMapZero | ||
| import Mathlib.Topology.ContinuousFunction.Weierstrass |
There was a problem hiding this comment.
How heavy are these new imports?
There was a problem hiding this comment.
The ContinuousMapZero file is probably just that file itself. The Unitization file pulls in Unitization and all the non-unital subobject stuff. So that's a bit heavier, but in my mind it's not too bad.
There was a problem hiding this comment.
Yeah, I guess that's not too bad.
leanprover-community-mathlib4-bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on:
|
leanprover-community-mathlib4-bot
added
the
merge-conflict
j-loreaux
removed
the
merge-conflict
|
bors r+ |
github-actions
bot
added
ready-to-merge
mathlib-bors bot
pushed a commit
that referenced
this pull request
May 29, 2024
…(s, 𝕜)₀` (#13326) This is a version of the Weierstrass approximation theorem for `C(s, 𝕜)₀`, and is necessary for instances of the non-unital continuous functional calculus. Co-authored by: @ADedecker - [ ] depends on: #13323
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
id is dense in C(s, 𝕜)₀id is dense in C(s, 𝕜)₀
callesonne
pushed a commit
that referenced
this pull request
Jun 4, 2024
…(s, 𝕜)₀` (#13326) This is a version of the Weierstrass approximation theorem for `C(s, 𝕜)₀`, and is necessary for instances of the non-unital continuous functional calculus. Co-authored by: @ADedecker - [ ] depends on: #13323
js2357
pushed a commit
that referenced
this pull request
Jun 18, 2024
…(s, 𝕜)₀` (#13326) This is a version of the Weierstrass approximation theorem for `C(s, 𝕜)₀`, and is necessary for instances of the non-unital continuous functional calculus. Co-authored by: @ADedecker - [ ] depends on: #13323
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is a version of the Weierstrass approximation theorem for
C(s, 𝕜)₀, and is necessary for instances of the non-unital continuous functional calculus.Co-authored by: @ADedecker
ContinuousMapZero#13323