Module

ValuationSubring_residue_injOn_pow_eq_one_and_exists_residue_eq_of_isAlgClosed.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_residue_injOn_pow_eq_one_and_exists_residue_eq_of_isAlgClosed

3 declarations indexed from sourceView source ↗

Module documentation

Valuation Subring residue inj On pow eq one and exists residue eq of is Alg Closed

Imports3

Mathlib.RingTheory.Valuation.ValuationSubring
Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed
Mathlib.Algebra.Ring.GeomSum

Imported by1

Nyll.AlgebraicCurves.Valuations.All

theorem

eq_one_of_pow_eq_one_of_residue_eq_one

L30 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_residue_injOn_pow_eq_one_and_exists_residue_eq_of_isAlgClosed.TeichmullerMuM.eq_one_of_pow_eq_one_of_residue_eq_one

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_residue_injOn_pow_eq_one_and_exists_residue_eq_of_isAlgClosed
open IsLocalRing
namespace TeichmullerMuM

Lean source · statement

theorem eq_one_of_pow_eq_one_of_residue_eq_one {R : Type*} [CommRing R] [IsLocalRing R] {m : ℕ}
    (hm : (m : ResidueField R) ≠ 0) {ζ : R} (hζ : ζ ^ m = 1) (h1 : residue R ζ = 1) : ζ = 1

theorem

eq_of_pow_eq_one_of_residue_eq

L41 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_residue_injOn_pow_eq_one_and_exists_residue_eq_of_isAlgClosed.TeichmullerMuM.eq_of_pow_eq_one_of_residue_eq

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_residue_injOn_pow_eq_one_and_exists_residue_eq_of_isAlgClosed
open IsLocalRing
namespace TeichmullerMuM

Lean source · statement

theorem eq_of_pow_eq_one_of_residue_eq {R : Type*} [CommRing R] [IsLocalRing R] {m : ℕ}
    (hm : (m : ResidueField R) ≠ 0) {ζ₁ ζ₂ : R} (h₁ : ζ₁ ^ m = 1) (h₂ : ζ₂ ^ m = 1)
    (h : residue R ζ₁ = residue R ζ₂) : ζ₁ = ζ₂

theorem

residue_injOn_pow_eq_one_and_exists_residue_eq_of_isAlgClosed

L58 ↗

ValuationSubring.residue_injOn_pow_eq_one_and_exists_residue_eq_of_isAlgClosed

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_residue_injOn_pow_eq_one_and_exists_residue_eq_of_isAlgClosed
open IsLocalRing
open TeichmullerMuM in

Lean source · statement

theorem _root_.ValuationSubring.residue_injOn_pow_eq_one_and_exists_residue_eq_of_isAlgClosed
    (K : Type*) [Field K] [IsAlgClosed K] (A : ValuationSubring K)
    (m : ℕ) (hm : (m : ResidueField ↥A) ≠ 0) :
    (∀ ζ₁ ζ₂ : ↥A, ζ₁ ^ m = 1 → ζ₂ ^ m = 1 → residue ↥A ζ₁ = residue ↥A ζ₂ → ζ₁ = ζ₂) ∧
    (∀ u : ResidueField ↥A, u ^ m = 1 → ∃ ζ : ↥A, ζ ^ m = 1 ∧ residue ↥A ζ = u)

Module documentation

Valuation Subring residue inj On pow eq one and exists residue eq of is Alg Closed

Declarations

eq_one_of_pow_eq_one_of_residue_eq_one

eq_of_pow_eq_one_of_residue_eq

residue_injOn_pow_eq_one_and_exists_residue_eq_of_isAlgClosed