ValuationSubring.mem_of_forall_mem_iff_of_subset
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_mem_of_forall_mem_iff_of_subset
open IsLocalRingLean source · statement
theorem _root_.ValuationSubring.mem_of_forall_mem_iff_of_subset
{F : Type*} [Field F] (K : Subfield F) (O V : ValuationSubring F)
(hKV : ∀ e ∈ K, e ∈ O → e ∈ V) (g : F)
(hg : ∀ V' : ValuationSubring F, (∀ e ∈ K, e ∈ V' ↔ e ∈ O) → g ∈ V') :
g ∈ V