instStarMul

Mathlib.Algebra.Star.NonUnitalSubalgebra

URI: https://scilib.ai/kg/mathlib#StarMemClass.instStarMul

Lean4

/-- In a star magma (i.e., a multiplication with an antimultiplicative involutive star
operation), any star-closed subset which is also closed under multiplication is itself a star
magma. -/
instance instStarMul {S R : Type*} [Mul R] [StarMul R] [SetLike S R] [MulMemClass S R] [StarMemClass S R] (s : S) :
    StarMul s where star_mul _ _ := Subtype.ext <| star_mul _ _

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

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

Разделы

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

Аффилиация

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