coe_span_singleton_eq_setOf_le_v_coe

English

For hv, x ∈ F there exists a ∈ O such that x = algebraMap a or x^{-1} = algebraMap a.

Русский

Пусть hv; для любого x ∈ F существует a ∈ O такой, что x = φ(a) или x^{-1} = φ(a).

LaTeX

$$∃ a ∈ O, x = algebraMap(O,F) a ∨ x^{-1} = algebraMap(O,F) a$$

Lean4

theorem coe_span_singleton_eq_setOf_le_v_coe (x : v.integer) :
    (Ideal.span { x } : Set v.integer) = {y : v.integer | v y ≤ v x} :=
  (Valuation.integer.integers v).coe_span_singleton_eq_setOf_le_v_algebraMap x

Похожие утверждения