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.
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(ring_theory/algebraic): algebraic extensions, algebraic elements #1519
feat(ring_theory/algebraic): algebraic extensions, algebraic elements #1519
Changes from 32 commits
40e74d7
790c892
c0633b5
931bf08
7fff9f3
e01a15e
2aff46a
d5c4897
71ed4b5
067984e
b64985a
25080c9
ca7c85d
542fca8
f3620a6
cac8632
6915af4
a4fb375
3079d38
4f0378c
a81fb91
62e7e1d
6f06db7
747a854
51ae389
d4c3d3d
e6f412f
38e46cb
1ffc6a4
267064b
5cb7a17
2c9afb2
303116b
b86edf4
9b46823
File filter
Filter by extension
Conversations
Jump to
There are no files selected for viewing
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is there a reason to introduce
is_algebraic
for subalgebras first? It looks like "compact subset" again.Why not just define
algebra.is_algebraic
directly and then say a subalgebra is algebraic if it is algebraic as an algebra?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Either way I think you will eventually want to prove that a subalgebra
S
is algebraic in the sense ofalgebra.is_algebraic
if and only if it is algebraic in the sense of this currentsubalgebra.is_algebraic
(right?). To mealgebra.is_algebraic
seems like the primary notion so defining it directly looks better.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
More or less done. They now all have elementwise definitions and
iff
s relating the various definitions.