mem_submonoid_iff — Mathlib

English

An element a lies in the units submonoid iff a is a unit in M.

Русский

Элемент a принадлежит подмоном единиц тогда и только тогда, когда a является единицей в M.

LaTeX

$$$a \\in \\text{IsUnit.submonoid}(M) \\iff \\text{IsUnit}(a)$$$

Lean4

@[to_additive]
theorem mem_submonoid_iff {M : Type*} [Monoid M] (a : M) : a ∈ IsUnit.submonoid M ↔ IsUnit a :=
  by
  change a ∈ setOf IsUnit ↔ IsUnit a
  rw [Set.mem_setOf_eq]

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