Theorems · Definition · field theory

IsAbelianGalois.recOn

{K : Type u_4} →
  {L : Type u_5} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          {motive : IsAbelianGalois K L → Sort u} →
            (t : IsAbelianGalois K L) →
              ([toIsGalois : IsGalois K L] → [toIsMulCommutative : IsMulCommutative Gal(L/K)] → motive ⋯) → motive t

Defined in: Mathlib.FieldTheory.Galois.Abelian
Cited by: 0 results in Mathlib
Foundations: Depth 48 from the axioms · uses propext, Quot.sound
Assumes: Field Field Algebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites6

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

Algebrastatement and proof · cited by 11,388
Fieldstatement and proof · cited by 7,404
AlgEquivstatement and proof · cited by 1,681
IsGaloisstatement and proof · cited by 149
IsMulCommutativestatement and proof · cited by 95
IsAbelianGaloisstatement and proof · cited by 10

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.