mul_mem

Mathlib.Algebra.Algebra.Subalgebra.Basic

URI: https://scilib.ai/kg/mathlib#Subalgebra.mul_mem

English

If x,y ∈ S, then x y ∈ S.

Русский

Если x,y ∈ S, то xy ∈ S.

LaTeX

$$$\forall x,y \in S, \ x y \in S$$$

Lean4

protected theorem mul_mem {x y : A} (hx : x ∈ S) (hy : y ∈ S) : x * y ∈ S :=
  mul_mem hx hy

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru