alexjbest

[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)

alexjbest

# 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

alexjbest

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
 -/

alexjbest

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):

alexjbest

#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'

alexjbest

{
	"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

alexjbest

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

alexjbest

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):

alexjbest

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

alexjbest

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