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]
theorem
SemiconjBy.add_right
{R : Type u}
[Distrib R]
{a : R}
{x : R}
{y : R}
{x' : R}
{y' : R}
(h : SemiconjBy a x y)
(h' : SemiconjBy a x' y')
:
SemiconjBy a (x + x') (y + y')
@[simp]
theorem
SemiconjBy.add_left
{R : Type u}
[Distrib R]
{a : R}
{b : R}
{x : R}
{y : R}
(ha : SemiconjBy a x y)
(hb : SemiconjBy b x y)
:
SemiconjBy (a + b) x y
theorem
SemiconjBy.neg_right
{R : Type u}
[Mul R]
[HasDistribNeg R]
{a : R}
{x : R}
{y : R}
(h : SemiconjBy a x y)
:
SemiconjBy a (-x) (-y)
@[simp]
theorem
SemiconjBy.neg_right_iff
{R : Type u}
[Mul R]
[HasDistribNeg R]
{a : R}
{x : R}
{y : R}
:
SemiconjBy a (-x) (-y) ↔ SemiconjBy a x y
theorem
SemiconjBy.neg_left
{R : Type u}
[Mul R]
[HasDistribNeg R]
{a : R}
{x : R}
{y : R}
(h : SemiconjBy a x y)
:
SemiconjBy (-a) x y
@[simp]
theorem
SemiconjBy.neg_left_iff
{R : Type u}
[Mul R]
[HasDistribNeg R]
{a : R}
{x : R}
{y : R}
:
SemiconjBy (-a) x y ↔ SemiconjBy a x y
theorem
SemiconjBy.neg_one_right
{R : Type u}
[MulOneClass R]
[HasDistribNeg R]
(a : R)
:
SemiconjBy a (-1) (-1)
theorem
SemiconjBy.neg_one_left
{R : Type u}
[MulOneClass R]
[HasDistribNeg R]
(x : R)
:
SemiconjBy (-1) x x
@[simp]
theorem
SemiconjBy.sub_right
{R : Type u}
[NonUnitalNonAssocRing R]
{a : R}
{x : R}
{y : R}
{x' : R}
{y' : R}
(h : SemiconjBy a x y)
(h' : SemiconjBy a x' y')
:
SemiconjBy a (x - x') (y - y')
@[simp]
theorem
SemiconjBy.sub_left
{R : Type u}
[NonUnitalNonAssocRing R]
{a : R}
{b : R}
{x : R}
{y : R}
(ha : SemiconjBy a x y)
(hb : SemiconjBy b x y)
:
SemiconjBy (a - b) x y