# mathlib3documentation

algebra.ring.semiconj

# Semirings and rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file gives lemmas about semirings, rings and domains. This is analogous to 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 algebra.ring.defs.

@[simp]
theorem semiconj_by.add_right {R : Type x} [distrib R] {a x y x' y' : R} (h : x y) (h' : x' y') :
(x + x') (y + y')
@[simp]
theorem semiconj_by.add_left {R : Type x} [distrib R] {a b x y : R} (ha : x y) (hb : x y) :
semiconj_by (a + b) x y
theorem semiconj_by.neg_right {R : Type x} [has_mul R] {a x y : R} (h : x y) :
(-x) (-y)
@[simp]
theorem semiconj_by.neg_right_iff {R : Type x} [has_mul R] {a x y : R} :
(-x) (-y) x y
theorem semiconj_by.neg_left {R : Type x} [has_mul R] {a x y : R} (h : x y) :
semiconj_by (-a) x y
@[simp]
theorem semiconj_by.neg_left_iff {R : Type x} [has_mul R] {a x y : R} :
semiconj_by (-a) x y x y
@[simp]
theorem semiconj_by.neg_one_right {R : Type x} (a : R) :
(-1) (-1)
@[simp]
theorem semiconj_by.neg_one_left {R : Type x} (x : R) :
semiconj_by (-1) x x
@[simp]
theorem semiconj_by.sub_right {R : Type x} {a x y x' y' : R} (h : x y) (h' : x' y') :
(x - x') (y - y')
@[simp]
theorem semiconj_by.sub_left {R : Type x} {a b x y : R} (ha : x y) (hb : x y) :
semiconj_by (a - b) x y