mathlib

4d59d4af - feat(number_theory): [S/P^e : R/p] = e * [S/P : R/p], where e is ramification index (#15316)

feat(number_theory): [S/P^e : R/p] = e * [S/P : R/p], where e is ramification index (#15316) Let `S` be a Dedekind domain extending the commutative ring `R`, `p` a maximal ideal of `R`, `P` a prime ideal of `S`, and `e` the (nonzero) ramification index of `P` over `p`. Because the ramification index is nonzero, we get an inclusion `R/p → S/P` and we can compute that the degree of the field extension `[S/(P^e) : R/p]` is exactly `e` times `[S/P : R/p]`. This is the next step in showing the fundamental identity of inertia degree and ramification index (#12287). Setting up the ingredients for the proof is quite complicated because it involves taking `(P^(i+1) / P^e)` as a `R/p`-subspace of `P^i / P^e` and basically each part of this structure would produce free metavariables if we naïvely assigned it an instance. In the end, the important parts are an instance for `S/(P^e)` as `R/p`-algebra and replacing subspaces with the image of inclusion maps. Co-authored-by: Anne Baanen <t.baanen@vu.nl> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>