-
Notifications
You must be signed in to change notification settings - Fork 330
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(Topology/Algebra/Field): ContinuousSMul
for intermediate fields
#18142
base: master
Are you sure you want to change the base?
feat(Topology/Algebra/Field): ContinuousSMul
for intermediate fields
#18142
Conversation
This reverts commit 1e083bf.
…tps://github.com/leanprover-community/mathlib4 into jiedong_jiang_continuous_smul_intermediate_field
…d' of https://github.com/leanprover-community/mathlib4 into jiedong_jiang_continuous_smul_intermediate_field" This reverts commit e3576a3, reversing changes made to ff465bf.
This reverts commit ff465bf.
PR summary f47c38cd66Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
The large import change is caused by the bot element of In order to solve this, I created a new file specialized for the |
!bench |
Here are the benchmark results for commit 774ee5e. |
move lemmas typo fix large import
4dd0f13
to
b5bd4dd
Compare
This reverts commit b5bd4dd.
!bench |
Here are the benchmark results for commit b0efef1. Benchmark Metric Change
========================================================================
- ~Mathlib.FieldTheory.Galois.Profinite instructions 30.9%
+ ~Mathlib.FieldTheory.IntermediateField.Algebraic instructions -22.7%
- ~Mathlib.FieldTheory.IntermediateField.Basic instructions 8.8%
+ ~Mathlib.NumberTheory.NumberField.Discriminant instructions -7.9% |
2 files, Instructions +4.0⬝10⁹
4 files, Instructions +1.0⬝10⁹
2 files, Instructions -2.0⬝10⁹
2 files, Instructions -4.0⬝10⁹
2 files, Instructions -6.0⬝10⁹
|
This PR/issue depends on: |
If
M
is an intermediate field between field extensionL/K
, thenM
acts continuously onL
and bot act continuously onM
. TheM
acts continuously onL
part is proved in a more general setup.