Mathlib.Algebra.Ring.Semiconj

Module docstring

{"# 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.

SemiconjBy.add_right theorem

[Distrib R] {a x y x' y' : R} (h : SemiconjBy a x y) (h' : SemiconjBy a x' y') : SemiconjBy a (x + x') (y + y')

Full source

@[simp]
theorem add_right [Distrib R] {a x y x' y' : R} (h : SemiconjBy a x y) (h' : SemiconjBy a x' y') :
    SemiconjBy a (x + x') (y + y') := by
  simp only [SemiconjBy, left_distrib, right_distrib, h.eq, h'.eq]

Additivity of Semiconjugacy Under Right Addition

Informal description

Let $R$ be a type with distributive multiplication over addition. For any elements $a, x, y, x', y' \in R$, if $x$ is semiconjugate to $y$ by $a$ (i.e., $a * x = y * a$) and $x'$ is semiconjugate to $y'$ by $a$ (i.e., $a * x' = y' * a$), then the sum $x + x'$ is semiconjugate to $y + y'$ by $a$, meaning that $a * (x + x') = (y + y') * a$.

SemiconjBy.add_left theorem

[Distrib R] {a b x y : R} (ha : SemiconjBy a x y) (hb : SemiconjBy b x y) : SemiconjBy (a + b) x y

Full source

@[simp]
theorem add_left [Distrib R] {a b x y : R} (ha : SemiconjBy a x y) (hb : SemiconjBy b x y) :
    SemiconjBy (a + b) x y := by
  simp only [SemiconjBy, left_distrib, right_distrib, ha.eq, hb.eq]

Additivity of Semiconjugacy Under Left Addition

Informal description

Let $R$ be a type with distributive multiplication over addition. For any elements $a, b, x, y \in R$, if $x$ is semiconjugate to $y$ by $a$ (i.e., $a * x = y * a$) and $x$ is semiconjugate to $y$ by $b$ (i.e., $b * x = y * b$), then $x$ is semiconjugate to $y$ by $a + b$, meaning that $(a + b) * x = y * (a + b)$.

SemiconjBy.neg_right theorem

(h : SemiconjBy a x y) : SemiconjBy a (-x) (-y)

Full source

theorem neg_right (h : SemiconjBy a x y) : SemiconjBy a (-x) (-y) := by
  simp only [SemiconjBy, h.eq, neg_mul, mul_neg]

Negation Preserves Semiconjugacy: $a * (-x) = (-y) * a$

Informal description

Let $R$ be a type with multiplication and negation. If $x$ is semiconjugate to $y$ by $a$ (i.e., $a * x = y * a$ holds), then $-x$ is semiconjugate to $-y$ by $a$, meaning that $a * (-x) = (-y) * a$.

SemiconjBy.neg_right_iff theorem

: SemiconjBy a (-x) (-y) ↔ SemiconjBy a x y

Full source

@[simp]
theorem neg_right_iff : SemiconjBySemiconjBy a (-x) (-y) ↔ SemiconjBy a x y :=
  ⟨fun h => neg_neg x ▸ neg_neg y ▸ h.neg_right, SemiconjBy.neg_right⟩

Negation Preserves Semiconjugacy: $a * (-x) = (-y) * a$ if and only if $a * x = y * a$

Informal description

For elements $a, x, y$ in a type with multiplication and negation, the element $x$ is semiconjugate to $y$ by $a$ (i.e., $a * x = y * a$) if and only if $-x$ is semiconjugate to $-y$ by $a$ (i.e., $a * (-x) = (-y) * a$).

SemiconjBy.neg_left theorem

(h : SemiconjBy a x y) : SemiconjBy (-a) x y

Full source

theorem neg_left (h : SemiconjBy a x y) : SemiconjBy (-a) x y := by
  simp only [SemiconjBy, h.eq, neg_mul, mul_neg]

Negation of Semiconjugating Element Preserves Semiconjugacy: $(-a) * x = y * (-a)$

Informal description

Let $R$ be a type with multiplication and negation. If $x$ is semiconjugate to $y$ by $a$ (i.e., $a * x = y * a$ holds), then $x$ is semiconjugate to $y$ by $-a$, meaning that $(-a) * x = y * (-a)$.

SemiconjBy.neg_left_iff theorem

: SemiconjBy (-a) x y ↔ SemiconjBy a x y

Full source

@[simp]
theorem neg_left_iff : SemiconjBySemiconjBy (-a) x y ↔ SemiconjBy a x y :=
  ⟨fun h => neg_neg a ▸ h.neg_left, SemiconjBy.neg_left⟩

Semiconjugacy Equivalence Under Negation: $(-a) * x = y * (-a) \leftrightarrow a * x = y * a$

Informal description

For elements $a, x, y$ in a type with multiplication and negation, $x$ is semiconjugate to $y$ by $-a$ if and only if $x$ is semiconjugate to $y$ by $a$. In other words, $(-a) * x = y * (-a)$ holds if and only if $a * x = y * a$ holds.

SemiconjBy.neg_one_right theorem

(a : R) : SemiconjBy a (-1) (-1)

Full source

theorem neg_one_right (a : R) : SemiconjBy a (-1) (-1) := by simp

Negation of One is Self-Semiconjugate in a Ring

Informal description

For any element $a$ in a ring $R$ with a distributive negation, the element $-1$ is semiconjugate to itself by $a$, i.e., $a * (-1) = (-1) * a$.

SemiconjBy.neg_one_left theorem

(x : R) : SemiconjBy (-1) x x

Full source

theorem neg_one_left (x : R) : SemiconjBy (-1) x x := by simp

Negation of One Semiconjugates Any Element to Itself

Informal description

For any element $x$ in a ring $R$ with a distributive negation, the element $-1$ semiconjugates $x$ to itself, i.e., $-1 * x = x * -1$.

SemiconjBy.sub_right theorem

(h : SemiconjBy a x y) (h' : SemiconjBy a x' y') : SemiconjBy a (x - x') (y - y')

Full source

@[simp]
theorem sub_right (h : SemiconjBy a x y) (h' : SemiconjBy a x' y') :
    SemiconjBy a (x - x') (y - y') := by
  simpa only [sub_eq_add_neg] using h.add_right h'.neg_right

Subtraction Preserves Semiconjugacy: $a * (x - x') = (y - y') * a$

Informal description

Let $R$ be a non-unital non-associative ring. For any elements $a, x, y, x', y' \in R$, if $x$ is semiconjugate to $y$ by $a$ (i.e., $a * x = y * a$) and $x'$ is semiconjugate to $y'$ by $a$ (i.e., $a * x' = y' * a$), then the difference $x - x'$ is semiconjugate to $y - y'$ by $a$, meaning that $a * (x - x') = (y - y') * a$.

SemiconjBy.sub_left theorem

(ha : SemiconjBy a x y) (hb : SemiconjBy b x y) : SemiconjBy (a - b) x y

Full source

@[simp]
theorem sub_left (ha : SemiconjBy a x y) (hb : SemiconjBy b x y) :
    SemiconjBy (a - b) x y := by
  simpa only [sub_eq_add_neg] using ha.add_left hb.neg_left

Semiconjugacy Preserved Under Left Subtraction in Non-unital Non-associative Rings

Informal description

Let $R$ be a non-unital non-associative ring. For any elements $a, b, x, y \in R$, if $x$ is semiconjugate to $y$ by $a$ (i.e., $a * x = y * a$) and $x$ is semiconjugate to $y$ by $b$ (i.e., $b * x = y * b$), then $x$ is semiconjugate to $y$ by $a - b$, meaning that $(a - b) * x = y * (a - b)$.