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] - [Merged by Bors] - feat(field_theory/adjoin): intermediate_field.to_subalgebra
distributes over supremum
#10937
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.
Thanks 🎉
bors merge
…utes over supremum (#10937) This PR proves `(E1 ⊔ E2).to_subalgebra = E1.to_subalgebra ⊔ E2.to_subalgebra`, under the assumption that `E1` and `E2` are finite-dimensional over `F`. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
Build failed (retrying...): |
bors r- |
Canceled. |
bors r+ |
begin | ||
let S1 := E1.to_subalgebra, | ||
let S2 := E2.to_subalgebra, | ||
refine le_antisymm (show _ ≤ (S1 ⊔ S2).to_intermediate_field _, from (sup_le (show S1 ≤ _, |
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 this is getting merged already, but what's the defeq going on in this show? Is there a lemma for it?
…utes over supremum (#10937) This PR proves `(E1 ⊔ E2).to_subalgebra = E1.to_subalgebra ⊔ E2.to_subalgebra`, under the assumption that `E1` and `E2` are finite-dimensional over `F`. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
intermediate_field.to_subalgebra
distributes over supremumintermediate_field.to_subalgebra
distributes over supremum
Pull request successfully merged into master. Build succeeded: |
intermediate_field.to_subalgebra
distributes over supremumintermediate_field.to_subalgebra
distributes over supremum
This PR proves
(E1 ⊔ E2).to_subalgebra = E1.to_subalgebra ⊔ E2.to_subalgebra
, under the assumption thatE1
andE2
are finite-dimensional overF
.