commMagma

Mathlib.Algebra.Group.InjSurj

URI: https://scilib.ai/kg/mathlib#Function.Injective.commMagma

Lean4

/-- A type endowed with `*` is a commutative magma, if it admits a surjective map that preserves
`*` from a commutative magma. -/
@[to_additive -- See note [reducible non-instances]
       /-- A type endowed with `+` is an additive commutative semigroup, if it admits
    a surjective map that preserves `+` from an additive commutative semigroup. -/
    ]
protected abbrev commMagma [CommMagma M₂] (f : M₁ → M₂) (hf : Injective f) (mul : ∀ x y, f (x * y) = f x * f y) :
    CommMagma M₁ where mul_comm x y := hf <| by rw [mul, mul, mul_comm]

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

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

Разделы

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

Аффилиация

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