Theorems · Definition · number theory

IsInertiaField.casesOn

{K : Type u_2} →
  {L : Type u_3} →
    {B : Type u_4} →
      [inst : Field K] →
        [inst_1 : Field L] →
          [inst_2 : Algebra K L] →
            [inst_3 : CommRing B] →
              {P : Ideal B} →
                {E : Type u_6} →
                  [inst_4 : Field E] →
                    [inst_5 : Algebra E L] →
                      [inst_6 : MulSemiringAction Gal(L/K) B] →
                        {motive : IsInertiaField K L P E → Sort u} →
                          (t : IsInertiaField K L P E) →
                            ([toIsGaloisGroup : IsGaloisGroup (↥(Ideal.inertia Gal(L/K) P)) E L] → motive ⋯) → motive t

Defined in: Mathlib.NumberTheory.RamificationInertia.HilbertTheory
Cited by: 1 results in Mathlib
Foundations: Depth 48 from the axioms · uses propext, Quot.sound
Assumes: Field Field Algebra CommRing Field Algebra MulSemiringAction

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CommRingstatement and proof · cited by 17,173
Algebrastatement and proof · cited by 11,388
Fieldstatement and proof · cited by 7,404
Idealstatement and proof · cited by 4,748
Subgroupstatement · cited by 3,593
AlgEquivstatement and proof · cited by 1,681
MulSemiringActionstatement and proof · cited by 423
IsGaloisGroupstatement and proof · cited by 96
Ideal.inertiastatement and proof · cited by 21
IsInertiaFieldstatement and proof · cited by 7

Cited by1

Results whose statement or proof uses this declaration.

isInertiaField_iffproof · cited by 1