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} :
semiconj_by (-a) x y ↔ semiconj_by a x y
@[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