NYLL
Module

Place_comap_algebraMap_ne_top.lean

Nyll.AlgebraicCurves.Places.Place_comap_algebraMap_ne_top
3 declarations indexed from sourceView source ↗

Module documentation

Place comap algebra Map ne top

Imports1
Imported by1

Declarations

theorem

algebraMap_ne_zero

L39 ↗
AlgebraicCurves.Places.Place_comap_algebraMap_ne_top.AlgebraicCurve.Place.algebraMap_ne_zero
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Place_comap_algebraMap_ne_top
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F'] [Algebra F F']
Lean source · statement
theorem algebraMap_ne_zero {f : F} (hf : f ≠ 0) : algebraMap F F' f ≠ 0
theorem

rowMain

L44 ↗
AlgebraicCurves.Places.Place_comap_algebraMap_ne_top.AlgebraicCurve.Place.rowMain
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Place_comap_algebraMap_ne_top
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F'] [Algebra F F']
variable (w : Place K F')
Lean source · statement
theorem rowMain [Algebra.IsIntegral F F'] :
    w.toValuationSubring.comap (algebraMap F F') ≠ ⊤
theorem

comap_algebraMap_ne_top

L70 ↗
AlgebraicCurve.Place.comap_algebraMap_ne_top
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Place_comap_algebraMap_ne_top
open IsDedekindDomain WithZero IsLocalRing
open _root_.AlgebraicCurve
  _root_.AlgebraicCurves.Places.Place_comap_algebraMap_ne_top.AlgebraicCurve in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.comap_algebraMap_ne_top {K F F' : Type*} [Field K] [Field F]
  [Field F'] [Algebra K F'] [Algebra F F'] (w : Place K F') [Algebra.IsIntegral F F'] :
    w.toValuationSubring.comap (algebraMap F F') ≠ ⊤

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