Module

ValuationRing_exists_ne_zero_forall_smul_eq_zero_of_module_finite.lean

Nyll.AlgebraicCurves.Valuations.ValuationRing_exists_ne_zero_forall_smul_eq_zero_of_module_finite

1 declaration indexed from sourceView source ↗

Module documentation

Valuation Ring exists ne zero forall smul eq zero of module finite

Imports6

Mathlib.RingTheory.Valuation.ValuationRing
Mathlib.RingTheory.Flat.TorsionFree
Mathlib.RingTheory.LocalRing.Module
Mathlib.Algebra.Module.Torsion.Basic
Mathlib.Algebra.Module.Projective
Mathlib.Tactic.Set

Imported by1

Nyll.AlgebraicCurves.Valuations.All

theorem

exists_ne_zero_forall_smul_eq_zero_of_module_finite

L31 ↗

ValuationRing.exists_ne_zero_forall_smul_eq_zero_of_module_finite

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationRing_exists_ne_zero_forall_smul_eq_zero_of_module_finite
open Submodule

Lean source · statement

theorem _root_.ValuationRing.exists_ne_zero_forall_smul_eq_zero_of_module_finite
    {R : Type*} [CommRing R] [IsDomain R] [ValuationRing R]
    {M : Type*} [AddCommGroup M] [Module R M] [Module.Finite R M] :
    ∃ a : R, a ≠ 0 ∧ ∀ m : M, (∃ c : R, c ≠ 0 ∧ c • m = 0) → a • m = 0

Module documentation

Valuation Ring exists ne zero forall smul eq zero of module finite

Declarations

exists_ne_zero_forall_smul_eq_zero_of_module_finite