toOpposite

Mathlib.Algebra.Group.Equiv.Opposite

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

Lean4

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

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

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

Разделы

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

Аффилиация

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