R : Type u
S : Type ?u.672918
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
⊢ LinearMap.ker (↑(aeval f) p) ⊓ LinearMap.ker (↑(aeval f) q) ≤ ⊥
R : Type u
S : Type ?u.672918
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
⊢ Disjoint (LinearMap.ker (↑(aeval f) p)) (LinearMap.ker (↑(aeval f) q))
rw [disjoint_iff_inf_le]
R : Type u
S : Type ?u.672918
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
v : M
hv : v ∈ LinearMap.ker (↑(aeval f) p) ⊓ LinearMap.ker (↑(aeval f) q)
⊢ v ∈ ⊥
R : Type u
S : Type ?u.672918
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
⊢ LinearMap.ker (↑(aeval f) p) ⊓ LinearMap.ker (↑(aeval f) q) ≤ ⊥
intro v hv
case intro.intro
R : Type u
S : Type ?u.672918
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker (↑(aeval f) p) ⊓ LinearMap.ker (↑(aeval f) q)
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ v ∈ ⊥
R : Type u
S : Type ?u.672918
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
v : M
hv : v ∈ LinearMap.ker (↑(aeval f) p) ⊓ LinearMap.ker (↑(aeval f) q)
⊢ v ∈ ⊥
rcases hpq with ⟨p', q', hpq'⟩
no goals
case intro.intro
R : Type u
S : Type ?u.672918
σ : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker (↑(aeval f) p) ⊓ LinearMap.ker (↑(aeval f) q)
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ v ∈ ⊥
simpa [LinearMap.mem_ker.1 (Submodule.mem_inf.1 hv).1,
  LinearMap.mem_ker.1 (Submodule.mem_inf.1 hv).2] using
  congr_arg (fun p : R[X] => aeval f p v) hpq'.symm