mem_submonoid_of_factors_subset_of_units_subset

English

If every factor of a is in a submonoid s and every unit of the ring is in s, then a ∈ s.

Русский

Если все делители a лежат в подмоноиде s, и все единицы кольца лежат в s, то a ∈ s.

LaTeX

$$$a \\\\neq 0 \\\\Rightarrow \\\\forall b \\, (b \in \text{factors}(a) \Rightarrow b \in s) \\\\Rightarrow \\\\forall c \in R^{\\times}, c \\in s \\\\Rightarrow a \\in s$$$

Lean4

theorem mem_submonoid_of_factors_subset_of_units_subset (s : Submonoid R) {a : R} (ha : a ≠ 0)
    (hfac : ∀ b ∈ factors a, b ∈ s) (hunit : ∀ c : Rˣ, (c : R) ∈ s) : a ∈ s :=
  by
  rcases (factors_spec a ha).2 with ⟨c, hc⟩
  rw [← hc]
  exact mul_mem (multiset_prod_mem _ hfac) (hunit _)

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