instMonoid — Mathlib

English

The units α^× form a monoid under multiplication with multiplication inherited from α.

Русский

Единицы α^× образуют моноид под умножением, где операция умножения наследуется от α.

LaTeX

$$$(\alpha^{\times}, \cdot) \text{ is a monoid}$$$

Lean4

@[to_additive]
instance instMonoid : Monoid αˣ :=
  {
    (inferInstance : MulOneClass
        αˣ) with
    mul_assoc := fun _ _ _ => ext <| mul_assoc _ _ _,
    npow := fun n a ↦
      { val := a ^ n
        inv := a⁻¹ ^ n
        val_inv := by rw [← a.commute_coe_inv.mul_pow]; simp
        inv_val := by rw [← a.commute_inv_coe.mul_pow]; simp }
    npow_zero := fun a ↦ by ext; simp
    npow_succ := fun n a ↦ by ext; simp [pow_succ] }

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