instGroupWithZero — Mathlib

English

The quaternion algebra ℍ[R] forms a group with zero under multiplication, i.e., it has an inverse for nonzero elements and zero behaves as a absorbing element.

Русский

Кватернионная алгебра ℍ[R] образует группу с нулём по умножению: у не нулевых элементов есть обратный, ноль поглощает.

LaTeX

$$ℍ[R] forms a GroupWithZero under multiplication$$

Lean4

instance instGroupWithZero : GroupWithZero ℍ[R] :=
  { Quaternion.instNontrivial with
    inv := Inv.inv
    inv_zero := by rw [inv_def, star_zero, smul_zero]
    mul_inv_cancel := fun a ha => by
      rw [inv_def, Algebra.mul_smul_comm (normSq a)⁻¹ a (star a), self_mul_star, smul_coe,
        inv_mul_cancel₀ (normSq_ne_zero.2 ha), coe_one] }

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