NYLL
Module

Place_deg_eq_one_iff_surjective_algebraMap_residueField.lean

Nyll.AlgebraicCurves.Places.Place_deg_eq_one_iff_surjective_algebraMap_residueField
2 declarations indexed from sourceView source ↗

Module documentation

Place deg eq one iff surjective algebra Map residue Field

Imports2
Imported by7

Declarations

theorem

deg_eq_one_iff_surjective_algebraMap_residueField_aux

L34 ↗
AlgebraicCurves.Places.Proofs.PlaceDegOneIffSurjectiveAlgebra.AlgebraicCurve.Place.deg_eq_one_iff_surjective_algebraMap_residueField_aux
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceDegOneIffSurjectiveAlgebra
open _root_.AlgebraicCurve
open _root_.ModularCurve
open scoped _root_.AlgebraicCurve _root_.AlgebraicCurve.Place in
Lean source · statement
theorem AlgebraicCurve.Place.deg_eq_one_iff_surjective_algebraMap_residueField_aux
    {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F) :
    v.deg = 1 ↔ Function.Surjective (algebraMap K v.ResidueField)
theorem

deg_eq_one_iff_surjective_algebraMap_residueField

L46 ↗
AlgebraicCurve.Place.deg_eq_one_iff_surjective_algebraMap_residueField
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceDegOneIffSurjectiveAlgebra
open _root_.AlgebraicCurve
open _root_.ModularCurve
open _root_.AlgebraicCurve
  _root_.AlgebraicCurves.Places.Proofs.PlaceDegOneIffSurjectiveAlgebra.AlgebraicCurve ModularCurve
  in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.deg_eq_one_iff_surjective_algebraMap_residueField {K F :
  Type*} [Field K] [Field F] [Algebra K F] (v : Place K F) :
    v.deg = 1 ↔ Function.Surjective (algebraMap K v.ResidueField)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.