English
For invertible a in α, the product of sym(a) with sym(a^{-1}) equals 1, showing that sym(a) is invertible with inverse sym(a^{-1}).
Русский
Для обратимого a в α произведение sym(a) и sym(a^{-1}) даёт 1, демонстрируя, что sym(a) обратно и имеет обратное sym(a^{-1}).
LaTeX
$$$\mathrm{sym}(a)\cdot \mathrm{sym}(a^{-1}) = 1$$$
Lean4
instance nonAssocSemiring [Semiring α] [Invertible (2 : α)] : NonAssocSemiring αˢʸᵐ :=
{ SymAlg.addCommMonoid with
one := 1
mul := (· * ·)
zero_mul := fun _ => by rw [mul_def, unsym_zero, zero_mul, mul_zero, add_zero, mul_zero, sym_zero]
mul_zero := fun _ => by rw [mul_def, unsym_zero, zero_mul, mul_zero, add_zero, mul_zero, sym_zero]
mul_one := fun _ => by rw [mul_def, unsym_one, mul_one, one_mul, ← two_mul, invOf_mul_cancel_left, sym_unsym]
one_mul := fun _ => by rw [mul_def, unsym_one, mul_one, one_mul, ← two_mul, invOf_mul_cancel_left, sym_unsym]
left_distrib := fun a b c =>
by
rw [mul_def, mul_def, mul_def, ← sym_add, ← mul_add, unsym_add, add_mul]
congr 2
rw [mul_add]
abel
right_distrib := fun a b c =>
by
rw [mul_def, mul_def, mul_def, ← sym_add, ← mul_add, unsym_add, add_mul]
congr 2
rw [mul_add]
abel }
