Theorems · Definition · number theory
FunctionField
(F : Type u_1) → (K : Type u_2) → [inst : Field F] → [inst_1 : Field K] → [Algebra (RatFunc F) K] → Prop
K is a function field over the field F if it is a finite
extension of the field of rational functions in one variable over F.
Note that K can be a function field over multiple, non-isomorphic, F.
- Defined in
- Mathlib.NumberTheory.FunctionField
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 110 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- FiniteDimensionalproof · cited by 1,854
- RatFuncstatement and proof · cited by 301
Cited by9
Results whose statement or proof uses this declaration.
- FunctionField.classNumberstatement and proof · cited by 1
- FunctionField.finiteDimensional_ratFunc_of_constantExtensionstatement and proof · cited by 1
- FunctionField.isAlgebraic_X_over_adjoin_transcendentalstatement and proof · cited by 1
- FunctionField.FiniteDimensional.adjoin_algebraMap_Xstatement and proof · cited by 1
- FunctionField.classNumber_eq_one_iffstatement and proof · cited by 0
- FunctionField.finiteDimensional_of_adjoin_transcendentalstatement and proof · cited by 0
- FunctionField.finiteDimensional_of_constantExtensionstatement and proof · cited by 0
- functionField_iffstatement and proof · cited by 0
- FunctionField.Algebra.IsAlgebraic.adjoin_algebraMap_Xstatement and proof · cited by 0