Theorems · Inductive type · field theory
FinTrdeg
(K : Type u_1) → (L : Type u_2) → [inst : Field K] → [inst_1 : Field L] → [Algebra K L] → Prop
A field extension L/K is said to have finite transcendence degree if there is some intermediate extension L/E/K with E/K finitely generated and L/E algebraic.
- Defined in
- Mathlib.FieldTheory.FinTrdeg
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 45 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by11
Results whose statement or proof uses this declaration.
- finTrdeg_iff_trdegstatement and proof · cited by 4
- trdeg_lt_aleph0statement and proof · cited by 3
- finite_of_isTranscendenceBasisstatement and proof · cited by 1
- exists_finset_isTranscendenceBasisstatement and proof · cited by 0
- FinTrdeg.casesOnstatement and proof · cited by 0
- FinTrdeg.exists_fg_isAlgebraicstatement and proof · cited by 0
- FinTrdeg.of_isTranscendenceBasisstatement · cited by 0
- FinTrdeg.of_trdegstatement · cited by 0
- FinTrdeg.recOnstatement and proof · cited by 0
- FinTrdeg.transstatement and proof · cited by 0
- finite_of_algebraicIndependentstatement and proof · cited by 0