ModulePlace_ord_eq_zero_of_isAlgebraic.lean
Nyll.AlgebraicCurves.Places.Place_ord_eq_zero_of_isAlgebraic
3 declarations indexed from sourceView source ↗ Module documentation
Place ord eq zero of is Algebraic
Declarations
AlgebraicCurves.Places.Proofs.Place_ord_eq_zero_of_isAlgebraic.AlgebraicCurve.Place.FF2R0.mem_of_isAlgebraic
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_eq_zero_of_isAlgebraic
noncomputable section
open Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace FF2R0
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : AlgebraicCurve.Place K F)
AlgebraicCurves.Places.Proofs.Place_ord_eq_zero_of_isAlgebraic.AlgebraicCurve.Place.FF2R0.ord_eq_zero_of_isAlgebraic'
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_eq_zero_of_isAlgebraic
noncomputable section
open Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace FF2R0
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : AlgebraicCurve.Place K F)
AlgebraicCurve.Place.ord_eq_zero_of_isAlgebraic
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_eq_zero_of_isAlgebraic
noncomputable section
open Polynomial