case left
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
⊢ IsLeftRegular p

case right
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
⊢ IsRightRegular p
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
⊢ IsRegular p
constructor
case left
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
q r : R[X]
h : (fun x => p * x) q = (fun x => p * x) r
⊢ q = r
case left
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
⊢ IsLeftRegular p
intro q r h
case left
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
q r : R[X]
h : p * q = p * r
⊢ q = r
case left
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
q r : R[X]
h : (fun x => p * x) q = (fun x => p * x) r
⊢ q = r
dsimp only at h
no goals
case left
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
q r : R[X]
h : p * q = p * r
⊢ q = r
rw [← sub_eq_zero, ← hp.mul_right_eq_zero_iff, mul_sub, h, sub_self]
case right
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
q r : R[X]
h : (fun x => x * p) q = (fun x => x * p) r
⊢ q = r
case right
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
⊢ IsRightRegular p
intro q r h
case right
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
q r : R[X]
h : q * p = r * p
⊢ q = r
case right
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
q r : R[X]
h : (fun x => x * p) q = (fun x => x * p) r
⊢ q = r
simp only at h
no goals
case right
R✝ : Type u
S : Type v
a b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Semiring R✝
p✝ : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
hp : Monic p
q r : R[X]
h : q * p = r * p
⊢ q = r
rw [← sub_eq_zero, ← hp.mul_left_eq_zero_iff, sub_mul, h, sub_self]