Documentation

Mathlib.Algebra.Ring.Semiconj

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