NYLL
Module

Place_isRational_iff_deg_eq_one.lean

Nyll.AlgebraicCurves.Places.Place_isRational_iff_deg_eq_one
1 declaration indexed from sourceView source ↗

Module documentation

Place isRational iff deg eq one

A place is rational exactly when its residue degree is one.

Imports1
Imported by25

Declarations

theorem

isRational_iff_deg_eq_one

L28 ↗
AlgebraicCurve.Place.isRational_iff_deg_eq_one
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_isRational_iff_deg_eq_one
open AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.Place.isRational_iff_deg_eq_one {K F : Type*} [Field K] [Field F]
  [Algebra K F] (v : Place K F) : v.IsRational ↔ v.deg = 1

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