leanprover-community
feat: Lindemann-Weierstrass Theorem
There's still a lot of work to be done before it gets into mathlib.
- [x] depends on: #6593
- [x] depends on: #6719
- [x] depends on: #6723
- [x] depends on: #6740
- [x] depends on: #7274
- [x] depends on: #8807
- [x] depends on: #12191
- [x] depends on: #12764
- [x] depends on: #16259
- [x] depends on: #16262
- [x] depends on: #16886
- [x] depends on: #16898
- [x] depends on: #16923
- [x] depends on: #16933
- [x] depends on: #17119
- [x] depends on: #17893
- [x] depends on: #17894
- [x] depends on: #17896
fyi @j-loreaux: I needed to add an instance from #5602 to fix the build here after merging master
That's fine. It should be back in after the update PR. I had only removed it so that the #5602 was cleanly reverted.
PR summary 094a2ab2c7
Import changes for modified files
No significant changes to the import graph
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.RingTheory.MvPolynomial.Symmetric.Eval (new file) |
1230 |
Mathlib.NumberTheory.Transcendental.Lindemann.SumAEvalARoots (new file) |
1231 |
Mathlib.FieldTheory.Minpoly.ConjRootClass (new file) |
1529 |
Mathlib.NumberTheory.Transcendental.Lindemann.AlgebraicPart (new file) |
1586 |
Mathlib.NumberTheory.Transcendental.Lindemann.Basic (new file) |
2384 |
Declarations diff
+ ConjRootClass
+ aevalMultiset
+ aevalMultiset_apply
+ aevalMultiset_map
+ aevalMultiset_map_of_card_eq
+ aevalMultiset_sumPolynomial
+ aeval_minpoly_iff
+ algebraicIndependent_exp
+ apply_mk
+ aroots_minpoly_eq_carrier_val
+ carrier
+ carrier_eq_mk_aroots_minpoly
+ carrier_zero
+ coe
+ coe_add
+ coe_apply
+ coe_injective
+ coe_single
+ coe_sum
+ coe_sumPolynomial
+ coe_toFinsupp
+ coe_zero
+ decidable
+ exist_mem_carrier_add_eq_zero
+ exists_sum_map_aroot_smul_eq
+ ind
+ instance : Coe (mapDomainFixed F R K) (ConjRootClass F K →₀ R)
+ instance : CoeFun (mapDomainFixed F R K) (fun _ ↦ ConjRootClass F K → R)
+ instance : InvolutiveNeg (ConjRootClass K L)
+ instance : IsEquiv L (IsConjRoot K)
+ instance : Neg (ConjRootClass K L) := ⟨Quotient.map (fun x ↦ -x) (fun _ _ ↦ IsConjRoot.neg)⟩
+ instance : Zero (ConjRootClass K L)
+ instance [Normal K L] [DecidableEq L] [Fintype (L ≃ₐ[K] L)] : DecidableEq (ConjRootClass K L)
+ irreducible_minpoly
+ liftFinsupp_mk
+ liftFinsupp_mk'
+ lift_eq_sum_toFinsupp
+ lift_mapRangeAlgHom_algebraMap
+ linearIndependent_exp
+ linearIndependent_exp_aux
+ linearIndependent_exp_aux2_1
+ linearIndependent_exp_aux2_2
+ linearIndependent_exp_aux_aroots_int
+ linearIndependent_exp_aux_aroots_rat
+ linearIndependent_exp_aux_int
+ linearIndependent_exp_aux_rat
+ linearIndependent_range_aux
+ mapDomainFixed
+ mapDomainFixedEquivSubtype
+ mem_carrier
+ mem_mapDomainFixed_iff
+ minpoly
+ minpoly.map_eq_prod
+ minpoly_inj
+ minpoly_injective
+ minpoly_mk
+ minpoly_ne_zero
+ mk
+ mk_apply_zero_eq
+ mk_eq_mk
+ mk_eq_zero_iff
+ mk_neg
+ mk_zero
+ monic_minpoly
+ nodup_aroots_minpoly
+ rootSet_minpoly_eq_carrier
+ scaleAEvalRoots
+ scaleAEvalRoots_apply
+ scaleAEvalRoots_eq_aevalMultiset
+ separable_minpoly
+ single
+ single_mul_single_apply_zero_eq_zero_iff
+ single_mul_single_apply_zero_ne_zero_iff
+ splits_minpoly
+ sumPolynomial
+ sum_single
+ toFinsupp
+ toFinsuppAux
+ toFinsuppAux_apply_apply_mk
+ transcendental_e
+ transcendental_exp
+ transcendental_log
+ transcendental_pi
+ zero_def
++ domCongrAut
++ instance [Normal K L] [DecidableEq L] [Fintype (L ≃ₐ[K] L)] (c : ConjRootClass K L) :
++ liftFinsupp
++ mapRangeAlgAut
++ mapRangeAlgEquiv
++ mapRangeAlgHom
++ mapRangeAlgHom_apply
++ mapRangeAlgHom_comp
++ mapRangeAlgHom_id
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>
The doc-module for script/declarations_diff.sh contains some details about this script.
Increase in tech debt: (relative, absolute) = (1.64, 0.00)
| Current number | Change | Type |
|---|---|---|
| 1717 | 1 | porting notes |
| 968 | 2 | erw |
Current commit 094a2ab2c7 Reference commit 274d91d783
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
![github-actions[bot] avatar](https://avatars.githubusercontent.com/in/15368?v=4 "Published by a pub.dev verified publisher"){kind=small}
This PR/issue depends on:
- ~~leanprover-community/mathlib4#6593~~
- ~~leanprover-community/mathlib4#6719~~
- ~~leanprover-community/mathlib4#6723~~
- ~~leanprover-community/mathlib4#6740~~
- ~~leanprover-community/mathlib4#7274~~
- ~~leanprover-community/mathlib4#8807~~
- ~~leanprover-community/mathlib4#12191~~
- ~~leanprover-community/mathlib4#12764~~
- ~~leanprover-community/mathlib4#16259~~
- ~~leanprover-community/mathlib4#16262~~
- ~~leanprover-community/mathlib4#16886~~
- ~~leanprover-community/mathlib4#16898~~
- ~~leanprover-community/mathlib4#16923~~
- ~~leanprover-community/mathlib4#16933~~
- ~~leanprover-community/mathlib4#17119~~
- ~~leanprover-community/mathlib4#17893~~
- ~~leanprover-community/mathlib4#17894~~
- ~~leanprover-community/mathlib4#17896~~
- ~~leanprover-community/mathlib4#18556~~
- leanprover-community/mathlib4#18693
- ~~leanprover-community/mathlib4#19225~~
- ~~leanprover-community/mathlib4#19246~~
- ~~leanprover-community/mathlib4#20092~~ By Dependent Issues (🤖). Happy coding!
This PR has been migrated to a fork-based workflow: https://github.com/leanprover-community/mathlib4/pull/28013