mathlib3 documentation

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 : semiconj_by a x y) (h' : semiconj_by a x' y') :
semiconj_by a (x + x') (y + y')
@[simp]
theorem semiconj_by.add_left {R : Type x} [distrib R] {a b x y : R} (ha : semiconj_by a x y) (hb : semiconj_by b x y) :
semiconj_by (a + b) x y
theorem semiconj_by.neg_right {R : Type x} [has_mul R] [has_distrib_neg R] {a x y : R} (h : semiconj_by a x y) :
semiconj_by a (-x) (-y)
@[simp]
theorem semiconj_by.neg_right_iff {R : Type x} [has_mul R] [has_distrib_neg R] {a x y : R} :
semiconj_by a (-x) (-y) semiconj_by a x y
theorem semiconj_by.neg_left {R : Type x} [has_mul R] [has_distrib_neg R] {a x y : R} (h : semiconj_by a x y) :
semiconj_by (-a) x y
@[simp]
theorem semiconj_by.neg_left_iff {R : Type x} [has_mul R] [has_distrib_neg R] {a x y : R} :
@[simp]
theorem semiconj_by.neg_one_right {R : Type x} [mul_one_class R] [has_distrib_neg R] (a : R) :
semiconj_by a (-1) (-1)
@[simp]
theorem semiconj_by.neg_one_left {R : Type x} [mul_one_class R] [has_distrib_neg R] (x : R) :
semiconj_by (-1) x x
@[simp]
theorem semiconj_by.sub_right {R : Type x} [non_unital_non_assoc_ring R] {a x y x' y' : R} (h : semiconj_by a x y) (h' : semiconj_by a x' y') :
semiconj_by a (x - x') (y - y')
@[simp]
theorem semiconj_by.sub_left {R : Type x} [non_unital_non_assoc_ring R] {a b x y : R} (ha : semiconj_by a x y) (hb : semiconj_by b x y) :
semiconj_by (a - b) x y