fromOpposite — Mathlib

Lean4
/-- A semigroup homomorphism `f : M →ₙ* N` such that `f x` commutes with `f y` for all `x, y`
defines a semigroup homomorphism from `Mᵐᵒᵖ`. -/
@[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 from `Mᵃᵒᵖ`. -/
    ]
def fromOpposite {M N : Type*} [Mul M] [Mul N] (f : M →ₙ* N) (hf : ∀ x y, Commute (f x) (f y)) : Mᵐᵒᵖ →ₙ* N
    where
  toFun := f ∘ MulOpposite.unop
  map_mul' _ _ := (f.map_mul _ _).trans (hf _ _).eq
Похожие утверждения