[feat(ring_theory/dedekind_domain/selmer_group): add Selmer groups of Dedekind domains](https://github.com/leanprover- community/mathlib/commit/9aec1a288c6222ef5ccfd02a07155e9dd37b20de) (mathlib#15405)
Authored-by: Multramate [(commit)](https://github.com/leanprover- community/mathlib/commit/9aec1a288c6222ef5ccfd02a07155e9dd37b20de)
| # 5 → 2 [data.buffer.parser, tactic.doc_commands] | |
| sed -i '/^import /{x;//!c\ | |
| import tactic.doc_commands | |
| d}' src/tactic/restate_axiom.lean | |
| # 9 → 8 [data.option.defs, data.rbmap.basic, data.rbtree.default_lt, logic.basic, tactic.cache] | |
| sed -i '/^import /{x;//!c\ | |
| import data.option.defs\ | |
| import data.rbmap.basic\ | |
| import logic.basic\ | |
| import tactic.cache |
| import all | |
| /- Checking 78317 declarations (plus 78402 automatically generated ones) in mathlib -/ | |
| /- The `generalisation_linter` linter reports: -/ | |
| /- typeclass generalisations may be possible -/ | |
| -- algebra/add_torsor.lean | |
| #print vsub_eq_sub /- _inst_1: add_group ↝ has_sub has_vsub | |
| -/ | |
| #print set.has_vsub /- T: add_torsor ↝ has_vsub | |
| -/ |
| INFO:werkzeug@2021-06-02 20:29:57,815: * Running on http://127.0.0.1:37777/ (Press CTRL+C to quit) | |
| ERROR:werkzeug@2021-06-02 20:30:02,778: 127.0.0.1 - - [02/Jun/2021 20:30:02] code 400, message Bad request version ('\x1a\x1a\x13\x01\x13\x02\x13\x03À+À/À,À0̨̩À\x13À\x14\x00\x9c\x00\x9d\x00/\x005\x01\x00\x01\x93ZZ\x00\x00\x00\x17\x00\x00ÿ\x01\x00\x01\x00\x00') | |
| INFO:werkzeug@2021-06-02 20:30:02,778: 127.0.0.1 - - [02/Jun/2021 20:30:02] "üñR<ÿ³ùEF*¦f¾ | |
| i"n}ùLIìäý ÷CÅmÕ | |
| .X)ýW À+À/À,À0̨̩ÀÀ7Ùί_YJ 4-M6ÀK_1#á{5*l#t | |
| mK ·éª¬VõÝÅk"zzÀ+À/À,À0̨̩ÀÀUsers/alex/lmfdb/lmfdb/ecnf/main.py", line 184, in <genexpr> | |
| ((nf, [url_for('.show_ecnf1', nf=nf), field_pretty(nf)]) | |
| File "sage/misc/cachefunc.pyx", line 1001, in sage.misc.cachefunc.CachedFunction.__call__ (build/cythonized/sage/misc/cachefunc.c:6100) | |
| File "/Users/alex/lmfdb/lmfdb/number_fields/web_number_field.py", line 221, in field_pretty | |
| if not is_fundamental_discriminant(D): |
| #print ProFiltPseuNormGrp.Top.of.compact_space | |
| #print differential_object.iso_of_components_inv_f | |
| #print add_monoid_hom.id_mem_filtration | |
| #print breen_deligne.universal_map.π_suitable | |
| #print Profinite.iso_of_homeo | |
| #print Mbar.ext_iff | |
| #print polyhedral_lattice.HomZ_map_equiv | |
| #print breen_deligne.data.system_res_def | |
| #print Mbar.Tinv_aux_ne_zero | |
| #print rescale.Tinv' |
| { | |
| "translatorID": "18AAAAAAA9afc-4cd6-8775-1980c3ce0fbf", | |
| "label": "Pretext pug export", | |
| "creator": "Alex J. Best", | |
| "target": "pug", | |
| "minVersion": "1.0.0", | |
| "maxVersion": "", | |
| "priority": 50, | |
| "displayOptions": { | |
| "exportNotes": true |
| import tactic.basic | |
| import tactic.apply | |
| import tactic.ring | |
| import tactic.abel | |
| import tactic.linarith | |
| import tactic.norm_num | |
| import data.rat.basic | |
| import data.rat.basic | |
| import data.real.basic | |
| import analysis.complex.exponential |
| p=7 | |
| L.<t> = FunctionField(GF(p)) | |
| S.<x,y> = L[] | |
| E = EllipticCurve(y^2 - x*(x-1)*(x-t^2)) | |
| deg = 3 # what degree correct up till | |
| R.<T>= PowerSeriesRing(QQ) | |
| lpol = ((1 + T) * (1 - T))^(-2) # bad factors computed by hand for now | |
| ll = [] | |
| for N in range(deg + 1): | |
| for pp in L.places(N): |
| import data.rat.basic | |
| import data.int.basic | |
| import data.nat.basic | |
| import algebra.field | |
| import linear_algebra.finsupp | |
| import ring_theory.polynomial | |
| import ring_theory.algebra | |
| import ring_theory.adjoin_root | |
| import ring_theory.ideals | |
| import algebra.module |
| import data.nat.basic | |
| import data.int.basic | |
| import data.int.modeq | |
| import init.data.fin.ops | |
| import data.zmod.basic | |
| import data.fintype | |
| import data.nat.prime | |
| import tactic.interactive | |
| import tactic.find | |
| import tactic.tidy |
