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 x y x' 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 b x 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 x 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 x y : R} : SemiconjBy a (-x) (-y) ↔ SemiconjBy a x y

theorem SemiconjBy.neg_left {R : Type u} [Mul R] [HasDistribNeg R] {a x 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 x 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 x y x' 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 b x y : R} (ha : SemiconjBy a x y) (hb : SemiconjBy b x y) : SemiconjBy (a - b) x y