Valuation.extendToLocalization.proof_2

theorem Valuation.extendToLocalization.proof_2 : ∀ {A : Type u_1} [inst : CommRing A] {Γ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ] (v : Valuation A Γ) {S : Submonoid A}, S ≤ v.supp.primeCompl → ∀ (s : ↥S), IsUnit (↑v.toMonoidWithZeroHom ↑s)

This theorem states that for any commutative ring `A`, any linearly ordered commutative group with zero `Γ`, any valuation `v` from `A` to `Γ`, and any submonoid `S` of `A`, if `S` is a subset of the complement of the prime ideal which is the support of `v`, then for any element `s` in `S`, the valuation of `s` is a unit. In other words, when a submonoid of a commutative ring is contained within the complement of the prime ideal formed by the vanishing points of a valuation, then the valuation of each element of the submonoid is invertible.

More concisely: If `S` is a submonoid of a commutative ring `A` that lies in the complement of the prime ideal generated by the support of a valuation `v` from `A` to a linearly ordered commutative group with zero `Γ`, then every element `s` in `S` is a unit with respect to `v`.