Module

Place_eq_of_toValuationSubring_le.lean

Nyll.AlgebraicCurves.Places.Place_eq_of_toValuationSubring_le

5 declarations indexed from sourceView source ↗

Module documentation

Place eq of to Valuation Subring le

Imports2

Imported by1

Nyll.AlgebraicCurves.Places.All

theorem

coe_unit_inv_eq_inv

L31 ↗

AlgebraicCurves.Places.Proofs.Place_eq_of_toValuationSubring_le.R1M3B.PlaceAux.coe_unit_inv_eq_inv

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_eq_of_toValuationSubring_le
namespace R1M3B
namespace PlaceAux
open AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem coe_unit_inv_eq_inv (O : ValuationSubring F) (u : (↥O)ˣ) :
    (((u⁻¹ : (↥O)ˣ) : O) : F) = (((u : O) : F))⁻¹

theorem

eq_inv_mul_inv_pow

L37 ↗

AlgebraicCurves.Places.Proofs.Place_eq_of_toValuationSubring_le.R1M3B.PlaceAux.eq_inv_mul_inv_pow

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_eq_of_toValuationSubring_le
namespace R1M3B
namespace PlaceAux
open AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem eq_inv_mul_inv_pow (O : ValuationSubring F) {f : F} (_hf : f ≠ 0) (hfinv : f⁻¹ ∈ O)
    {ϖ : O} (u : (↥O)ˣ) (m : ℕ) (hu : (⟨f⁻¹, hfinv⟩ : O) = u * ϖ ^ m) :
    f = (((u⁻¹ : (↥O)ˣ) : O) : F) * (((ϖ : F))⁻¹) ^ m

theorem

eq_of_le

L45 ↗

AlgebraicCurves.Places.Proofs.Place_eq_of_toValuationSubring_le.R1M3B.PlaceAux.eq_of_le

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_eq_of_toValuationSubring_le
namespace R1M3B
namespace PlaceAux
open AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem eq_of_le {v w : Place K F} (h : v.toValuationSubring ≤ w.toValuationSubring) : v = w

theorem

forall_mem_iff_of_forall_mem_imp

L102 ↗

AlgebraicCurves.Places.Proofs.Place_eq_of_toValuationSubring_le.R1M3B.PlaceAux.forall_mem_iff_of_forall_mem_imp

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_eq_of_toValuationSubring_le
namespace R1M3B
namespace PlaceAux
open AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem forall_mem_iff_of_forall_mem_imp
    {F' : Type*} [Field F'] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
      [Algebra.IsIntegral F F']
    (v w : Place K F')
    (himp : ∀ f : F, algebraMap F F' f ∈ v.toValuationSubring → algebraMap F F' f ∈
      w.toValuationSubring) :
    ∀ f : F, algebraMap F F' f ∈ v.toValuationSubring ↔ algebraMap F F' f ∈ w.toValuationSubring

theorem

eq_of_toValuationSubring_le

L118 ↗

AlgebraicCurve.Place.eq_of_toValuationSubring_le

Source context 2 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_eq_of_toValuationSubring_le

Lean source · statement

theorem _root_.AlgebraicCurve.Place.eq_of_toValuationSubring_le
    {K F : Type*} [Field K] [Field F] [Algebra K F] {v w : AlgebraicCurve.Place K F}
    (h : v.toValuationSubring ≤ w.toValuationSubring) : v = w

Module documentation

Place eq of to Valuation Subring le

Declarations

coe_unit_inv_eq_inv

eq_inv_mul_inv_pow

eq_of_le

forall_mem_iff_of_forall_mem_imp

eq_of_toValuationSubring_le