/
Semiconj.lean
102 lines (72 loc) · 3.14 KB
/
Semiconj.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
/-
Copyright (c) 2014 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Yury Kudryashov, Neil Strickland
-/
import Mathlib.Algebra.Group.Semiconj.Defs
import Mathlib.Algebra.Ring.Defs
#align_import algebra.ring.semiconj from "leanprover-community/mathlib"@"70d50ecfd4900dd6d328da39ab7ebd516abe4025"
/-!
# 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`.
-/
universe u v w x
variable {α : Type u} {β : Type v} {γ : Type w} {R : Type x}
open Function
namespace SemiconjBy
@[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]
#align semiconj_by.add_right SemiconjBy.add_right
@[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]
#align semiconj_by.add_left SemiconjBy.add_left
section
variable [Mul R] [HasDistribNeg R] {a x y : R}
theorem neg_right (h : SemiconjBy a x y) : SemiconjBy a (-x) (-y) := by
simp only [SemiconjBy, h.eq, neg_mul, mul_neg]
#align semiconj_by.neg_right SemiconjBy.neg_right
@[simp]
theorem neg_right_iff : SemiconjBy a (-x) (-y) ↔ SemiconjBy a x y :=
⟨fun h => neg_neg x ▸ neg_neg y ▸ h.neg_right, SemiconjBy.neg_right⟩
#align semiconj_by.neg_right_iff SemiconjBy.neg_right_iff
theorem neg_left (h : SemiconjBy a x y) : SemiconjBy (-a) x y := by
simp only [SemiconjBy, h.eq, neg_mul, mul_neg]
#align semiconj_by.neg_left SemiconjBy.neg_left
@[simp]
theorem neg_left_iff : SemiconjBy (-a) x y ↔ SemiconjBy a x y :=
⟨fun h => neg_neg a ▸ h.neg_left, SemiconjBy.neg_left⟩
#align semiconj_by.neg_left_iff SemiconjBy.neg_left_iff
end
section
variable [MulOneClass R] [HasDistribNeg R] {a x y : R}
-- Porting note: `simpNF` told me to remove `simp` attribute
theorem neg_one_right (a : R) : SemiconjBy a (-1) (-1) :=
(one_right a).neg_right
#align semiconj_by.neg_one_right SemiconjBy.neg_one_right
-- Porting note: `simpNF` told me to remove `simp` attribute
theorem neg_one_left (x : R) : SemiconjBy (-1) x x :=
(SemiconjBy.one_left x).neg_left
#align semiconj_by.neg_one_left SemiconjBy.neg_one_left
end
section
variable [NonUnitalNonAssocRing R] {a b x y x' y' : R}
@[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
#align semiconj_by.sub_right SemiconjBy.sub_right
@[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
#align semiconj_by.sub_left SemiconjBy.sub_left
end
end SemiconjBy