Semirings and rings #
This file gives lemmas about semirings, rings and domains.
This is analogous to Mathlib/Algebra/Group/Basic.lean
,
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.lean
.
theorem
Commute.mul_self_eq_mul_self_iff
{R : Type u}
[NonUnitalNonAssocRing R]
[NoZeroDivisors R]
{a b : R}
(h : Commute a b)
:
@[simp]
@[simp]
theorem
Commute.neg_one_right
{R : Type u}
[MulOneClass R]
[HasDistribNeg R]
(a : R)
:
Commute a (-1)
@[simp]
@[simp]
Alias of neg_sq
.
Alias of neg_one_sq
.
theorem
mul_self_eq_mul_self_iff
{R : Type u}
[NonUnitalNonAssocCommRing R]
[NoZeroDivisors R]
{a b : R}
:
@[instance 100]