Theorems · Definition · number theory

Ideal.inertiaDegIn

{A : Type u_1} → [inst : CommRing A] → Ideal A → (B : Type u_2) → [inst_1 : CommRing B] → [Algebra A B] → ℕ

If L / K is a Galois extension, it can be seen from the theorem Ideal.inertiaDeg_eq_of_isGaloisGroup that all Ideal.inertiaDeg over a fixed maximal ideal p of A are the same, which we define as Ideal.inertiaDegIn.

Defined in

Mathlib.NumberTheory.RamificationInertia.Galois

Cited by

18 results in Mathlib

Foundations

Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebra