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