Semirings and rings #
This file gives lemmas about semirings, rings and domains.
This is analogous to Mathlib.Algebra.Group.Basic
,
the difference being that the former is about +
and *
separately, while
the present file is about their interaction.
For the definitions of semirings and rings see Mathlib.Algebra.Ring.Defs
.
@[simp]
@[simp]
theorem
Commute.neg_one_right
{R : Type u}
[MulOneClass R]
[HasDistribNeg R]
(a : R)
:
Commute a (-1)
@[simp]
@[simp]
Alias of neg_one_sq
.
@[instance 100]