valueMonoid_eq_valueGroup — Mathlib

English

In the commutative case, y ∈ valueGroup f iff there exists a with f a ≠ 0 and some x with f a · y = f x.

Русский

В коммутативном случае y ∈ valueGroup f тогда и только тогда, когда существует a такое, что f a ≠ 0 и существует x, что f a · y = f x.

LaTeX

$$y ∈ valueGroup f ↔ ∃ a, f a ≠ 0 ∧ ∃ x, f a · y = f x$$

Lean4

theorem valueMonoid_eq_valueGroup : (valueMonoid f) = (valueGroup f).toSubmonoid :=
  by
  rw [valueGroup_def, Subgroup.closure_toSubmonoid, Eq.comm]
  apply Submonoid.closure_eq_of_le
  · simp only [union_subset_iff, subset_refl, true_and]
    intro _ ⟨y, hy⟩
    use y⁻¹
    simp [hy]
  · simp [Submonoid.closure_union]

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