Module

ValuationSubring_residueValuationSubring_valuation_lt_one_iff.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_residueValuationSubring_valuation_lt_one_iff

3 declarations indexed from sourceView source ↗

Module documentation

Valuation Subring residue Valuation Subring valuation lt one iff

Imports1

Nyll.AlgebraicCurves.Valuations.ValuationSubring_ResidueValuationSubring

Imported by1

Nyll.AlgebraicCurves.Valuations.All

theorem

isUnit_iff

L30 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_residueValuationSubring_valuation_lt_one_iff.CompVUnitSol.isUnit_iff

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_residueValuationSubring_valuation_lt_one_iff
open IsLocalRing
namespace CompVUnitSol
variable {L : Type*} [Field L] (A S : ValuationSubring L) (h : A ≤ S)

Lean source · statement

theorem isUnit_iff (a : A) : IsUnit (A.toResidueValuationSubring S h a) ↔ IsUnit a

theorem

valuation_lt_one_iff

L51 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_residueValuationSubring_valuation_lt_one_iff.CompVUnitSol.valuation_lt_one_iff

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_residueValuationSubring_valuation_lt_one_iff
open IsLocalRing
namespace CompVUnitSol
variable {L : Type*} [Field L] (A S : ValuationSubring L) (h : A ≤ S)

Lean source · statement

theorem valuation_lt_one_iff (a : A) :
    (A.residueValuationSubring S h).valuation (residue S (A.inclusion S h a)) < 1 ↔
      A.valuation (a : L) < 1

theorem

residueValuationSubring_valuation_lt_one_iff

L60 ↗

ValuationSubring.residueValuationSubring_valuation_lt_one_iff

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_residueValuationSubring_valuation_lt_one_iff
open IsLocalRing

Lean source · statement

theorem _root_.ValuationSubring.residueValuationSubring_valuation_lt_one_iff
    {L : Type*} [Field L] (A S : ValuationSubring L) (h : A ≤ S) (a : A) :
    (A.residueValuationSubring S h).valuation (IsLocalRing.residue S (A.inclusion S h a)) < 1 ↔
      A.valuation (a : L) < 1

Module documentation

Valuation Subring residue Valuation Subring valuation lt one iff

Declarations

isUnit_iff

valuation_lt_one_iff

residueValuationSubring_valuation_lt_one_iff