nonunits_le_nonunits — Mathlib

English

For valuation subrings A,B, B.nonunits ⊆ A.nonunits if and only if A ≤ B.

Русский

Для подкольц A,B: B.nonunits ⊆ A.nonunits тогда и только тогда, когда A ⊆ B.

LaTeX

$$$B_{\mathrm{nonunits}} \subseteq A_{\mathrm{nonunits}} \iff A \subseteq B$$$

Lean4

theorem nonunits_le_nonunits {A B : ValuationSubring K} : B.nonunits ≤ A.nonunits ↔ A ≤ B :=
  by
  constructor
  · intro h x hx
    by_cases h_1 : x = 0; · simp only [h_1, zero_mem]
    rw [← valuation_le_one_iff, ← not_lt, Valuation.one_lt_val_iff _ h_1] at hx ⊢
    by_contra h_2; exact hx (h h_2)
  · intro h x hx
    by_contra h_1; exact not_lt.2 (monotone_mapOfLE _ _ h (not_lt.1 h_1)) hx

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