isSymmOp_of_isCommutative

Mathlib.Logic.OpClass

URI: https://scilib.ai/kg/mathlib#isSymmOp_of_isCommutative

← MathLib Explorer

English

If an operation is commutative, then it is a symmetric operation.

Русский

Если операция коммутативна, то она симметрична.

LaTeX

$$$\forall \alpha, (op:\, \alpha \to \alpha \to \alpha), [\text{Std.Commutative}(op)] \Rightarrow \text{IsSymmOp}(op)$$$

Lean4

instance (priority := 100) isSymmOp_of_isCommutative (α : Sort u) (op : α → α → α) [Std.Commutative op] : IsSymmOp op
    where symm_op := Std.Commutative.comm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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