## Stream: new members

### Topic: Proving that an element is an integer of a valuation ring

#### Stepan Nesterov (Feb 10 2023 at 05:00):

Let's say I want to write down an element of a ring docs#valuation.integer. I try doing it like this:

import ring_theory.valuation.basic
import algebra.order.monoid.with_zero.defs
variables {R : Type*} [comm_ring R] {w : valuation R ℤₘ₀}
def my_integer (a : R) (ha : w a = 0) : w.integer := ⟨a, begin rw set.mem_def, end⟩


but get a message

rewrite tactic failed, did not find instance of the pattern in the target expression
?m_2 ∈ ?m_3


#### Stepan Nesterov (Feb 10 2023 at 05:02):

How do I figure out what the right ∈ is, so that I can rw it?

#### Gareth Ma (Feb 10 2023 at 06:01):

import ring_theory.valuation.basic
import ring_theory.valuation.integers
import algebra.order.monoid.with_zero.defs

open_locale discrete_valuation

variables {R : Type*} [comm_ring R] {w : valuation R ℤₘ₀}
example (a : R) (ha : w a = 0) : a ∈ w.integer :=
begin
simp only [valuation.integer, subring.mem_mk, mem_set_of_eq, ha, zero_le_one],
end


#### Adam Topaz (Feb 10 2023 at 14:43):

@Stepan Nesterov can you please provide a working #mwe ?

#### Adam Topaz (Feb 10 2023 at 14:49):

Anyway, it seems like whoever wrote this part of the valuation theory library forgot to make a valuation.mem_integer lemma.
The following is (approximately) what I would do in this case.

import ring_theory.valuation.integers

variables {R Γ : Type*} [comm_ring R] [linear_ordered_comm_group_with_zero Γ] {w : valuation R Γ}

lemma valuation.mem_integer_iff (a : R) : a ∈ w.integer ↔ w a ≤ 1 := iff.rfl

example (a : R) (ha : w a = 0) : a ∈ w.integer :=
begin
rw [valuation.mem_integer_iff, ha],
exact zero_le_one,
end


Last updated: Dec 20 2023 at 11:08 UTC