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
[Merged by Bors] - chore: Slightly modify the split of CanonicalEmbedding
#11917
Conversation
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.
lgtm, one comment
@@ -507,5 +507,3 @@ theorem mem_span_fractionalIdealLatticeBasis (x : (E K)) : | |||
rfl | |||
|
|||
end integerLattice | |||
|
|||
end NumberField.mixedEmbedding |
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.
I know it's not necessary, strictly speaking, but I'd keep this line.
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.
Yes. you're right.
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.
LGTM
bors d+
The canonical embedding of a number field `K` of degree `n` is the ring homomorphism | ||
`K →+* ℂ^n` that sends `x ∈ K` to `(φ_₁(x),...,φ_n(x))` where the `φ_i`'s are the complex | ||
embeddings of `K`. Note that we do not choose an ordering of the embeddings, but instead map `K` | ||
into the type `(K →+* ℂ) → ℂ` of `ℂ`-vectors indexed by the complex embeddings. |
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.
Was this intentionally duplicated from the Basic
file?
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.
Yeah, you're right, that's not optimal. I'll change to a better docstring. Thanks
✌️ xroblot can now approve this pull request. To approve and merge a pull request, simply reply with |
bors + |
Did you mean "r+"? |
bors r+ |
Create a new directory for the split of `CanonicalEmbedding` since more material is coming. Also add some docstrings.
Pull request successfully merged into master. Build succeeded: |
CanonicalEmbedding
CanonicalEmbedding
Create a new directory for the split of `CanonicalEmbedding` since more material is coming. Also add some docstrings.
Create a new directory for the split of `CanonicalEmbedding` since more material is coming. Also add some docstrings.
Create a new directory for the split of `CanonicalEmbedding` since more material is coming. Also add some docstrings.
Create a new directory for the split of `CanonicalEmbedding` since more material is coming. Also add some docstrings.
Create a new directory for the split of
CanonicalEmbedding
since more material is coming.Also add some docstrings.