invMonoidHom — Mathlib

English

For a commutative group α, and integer n, the map x ↦ x^n is a group homomorphism α → α.

Русский

Для коммутативной группы α и целого числа n отображение x ↦ x^n является гомоморфизмом групп α → α.

LaTeX

$$$\\text{zpowGroupHom}(n) : α \\to^* α$ with $\\text{toFun}(x) = x^n$, $\\text{map_one'} = 1$, $\\text{map_mul'}(a,b) = a^n b^n = (ab)^n$.$$

Lean4

/-- Inversion on a commutative group, considered as a monoid homomorphism. -/
@[to_additive /-- Negation on a commutative additive group, considered as an additive monoid
    homomorphism. -/
    ]
def invMonoidHom : α →* α where
  toFun := Inv.inv
  map_one' := inv_one
  map_mul' := mul_inv

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