mul_mem_units — Mathlib

English

Let S be a submonoid of M. If x and y are units in S, then their product x*y is also a unit in S.

Русский

Пусть S — подмонад M. Если x и y — единицы в S, то их произведение x*y также является единицей в S.

LaTeX

$$$ x \in S.units \land y \in S.units \implies x \cdot y \in S.units $$$

Lean4

@[to_additive]
theorem mul_mem_units (S : Submonoid M) {x y : Mˣ} (h₁ : x ∈ S.units) (h₂ : y ∈ S.units) : x * y ∈ S.units :=
  mul_mem h₁ h₂

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