Mathlib Map

Theorems · Inductive type · field theory

IsSepClosure

(k : Type u) → [inst : Field k] → (K : Type v) → [inst_1 : Field K] → [Algebra k K] → Prop

Typeclass for an extension being a separable closure.

Defined in
Mathlib.FieldTheory.IsSepClosed
Cited by
3 results in Mathlib
Foundations
Depth 45 from the axioms · uses propext, Quot.sound
Assumes
FieldFieldAlgebra
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

IsSepClosure.separable · cited by 2IsSepClosure.separableIsSepClosure.sep_closed · cited by 1IsSepClosure.sep_closedIsSepClosure.casesOn · cited by 0IsSepClosure.casesOnIsSepClosure.equiv · cited by 0IsSepClosure.equivIsSepClosure.recOn · cited by 0IsSepClosure.recOnisSepClosure_iff · cited by 0isSepClosure_iffAlgebra · cited by 11388AlgebraField · cited by 7404FieldIsSepClosureCITED BYCITES

Cites2

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

  • Algebrastatement · cited by 11,388
  • Fieldstatement · cited by 7,404

Cited by6

Results whose statement or proof uses this declaration.