toOpposite

Mathlib.Algebra.Group.Equiv.Opposite

URI: https://scilib.ai/kg/mathlib#MulHom.toOpposite

Lean4

/-- A semigroup homomorphism `f : M →ₙ* N` such that `f x` commutes with `f y` for all `x, y`
defines a semigroup homomorphism to `Nᵐᵒᵖ`. -/
@[to_additive (attr := simps -fullyApplied) /--
    An additive semigroup homomorphism `f : AddHom M N` such that `f x` additively
    commutes with `f y` for all `x, y` defines an additive semigroup homomorphism to `Sᵃᵒᵖ`. -/
    ]
def toOpposite {M N : Type*} [Mul M] [Mul N] (f : M →ₙ* N) (hf : ∀ x y, Commute (f x) (f y)) : M →ₙ* Nᵐᵒᵖ
    where
  toFun := op ∘ f
  map_mul' x y := by simp [(hf x y).eq]

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

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

Разделы

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

Аффилиация

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