[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : (n : ℕ) → M ⧸ I ^ n • ⊤
m n : ℕ
h : m ≤ n
⊢ I ^ n • ⊤ ≤ LinearMap.ker (mkQ (I ^ m • ⊤))
[PROOFSTEP]
rw [ker_mkQ]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : (n : ℕ) → M ⧸ I ^ n • ⊤
m n : ℕ
h : m ≤ n
⊢ I ^ n • ⊤ ≤ I ^ m • ⊤
[PROOFSTEP]
exact smul_mono (Ideal.pow_le_pow h) le_rfl
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
a✝ b✝ : (n : ℕ) → M ⧸ I ^ n • ⊤
hf :
  a✝ ∈
    {f |
      ∀ {m n : ℕ} (h : m ≤ n),
        ↑(liftQ (I ^ n • ⊤) (mkQ (I ^ m • ⊤)) (_ : I ^ n • ⊤ ≤ LinearMap.ker (mkQ (I ^ m • ⊤)))) (f n) = f m}
hg :
  b✝ ∈
    {f |
      ∀ {m n : ℕ} (h : m ≤ n),
        ↑(liftQ (I ^ n • ⊤) (mkQ (I ^ m • ⊤)) (_ : I ^ n • ⊤ ≤ LinearMap.ker (mkQ (I ^ m • ⊤)))) (f n) = f m}
m n : ℕ
hmn : m ≤ n
⊢ ↑(liftQ (I ^ n • ⊤) (mkQ (I ^ m • ⊤)) (_ : I ^ n • ⊤ ≤ LinearMap.ker (mkQ (I ^ m • ⊤)))) ((a✝ + b✝) n) = (a✝ + b✝) m
[PROOFSTEP]
rw [Pi.add_apply, Pi.add_apply, LinearMap.map_add, hf hmn, hg hmn]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
m✝ n✝ : ℕ
hmn : m✝ ≤ n✝
⊢ ↑(liftQ (I ^ n✝ • ⊤) (mkQ (I ^ m✝ • ⊤)) (_ : I ^ n✝ • ⊤ ≤ LinearMap.ker (mkQ (I ^ m✝ • ⊤)))) (OfNat.ofNat 0 n✝) =
    OfNat.ofNat 0 m✝
[PROOFSTEP]
rw [Pi.zero_apply, Pi.zero_apply, LinearMap.map_zero]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
c : R
f : (n : ℕ) → M ⧸ I ^ n • ⊤
hf :
  f ∈
    {
          toAddSubsemigroup :=
            {
              carrier :=
                {f |
                  ∀ {m n : ℕ} (h : m ≤ n),
                    ↑(liftQ (I ^ n • ⊤) (mkQ (I ^ m • ⊤)) (_ : I ^ n • ⊤ ≤ LinearMap.ker (mkQ (I ^ m • ⊤)))) (f n) =
                      f m},
              add_mem' :=
                (_ :
                  ∀ {a b : (n : ℕ) → M ⧸ I ^ n • ⊤},
                    a ∈
                        {f |
                          ∀ {m n : ℕ} (h : m ≤ n),
                            ↑(liftQ (I ^ n • ⊤) (mkQ (I ^ m • ⊤)) (_ : I ^ n • ⊤ ≤ LinearMap.ker (mkQ (I ^ m • ⊤))))
                                (f n) =
                              f m} →
                      b ∈
                          {f |
                            ∀ {m n : ℕ} (h : m ≤ n),
                              ↑(liftQ (I ^ n • ⊤) (mkQ (I ^ m • ⊤)) (_ : I ^ n • ⊤ ≤ LinearMap.ker (mkQ (I ^ m • ⊤))))
                                  (f n) =
                                f m} →
                        ∀ (m n : ℕ) (hmn : m ≤ n),
                          ↑(liftQ (I ^ n • ⊤) (mkQ (I ^ m • ⊤)) (_ : I ^ n • ⊤ ≤ LinearMap.ker (mkQ (I ^ m • ⊤))))
                              ((a + b) n) =
                            (a + b) m) },
          zero_mem' :=
            (_ :
              ∀ {m n : ℕ} (hmn : m ≤ n),
                ↑(liftQ (I ^ n • ⊤) (mkQ (I ^ m • ⊤)) (_ : I ^ n • ⊤ ≤ LinearMap.ker (mkQ (I ^ m • ⊤))))
                    (OfNat.ofNat 0 n) =
                  OfNat.ofNat 0 m) }.toAddSubsemigroup.carrier
m n : ℕ
hmn : m ≤ n
⊢ ↑(liftQ (I ^ n • ⊤) (mkQ (I ^ m • ⊤)) (_ : I ^ n • ⊤ ≤ LinearMap.ker (mkQ (I ^ m • ⊤)))) ((c • f) n) = (c • f) m
[PROOFSTEP]
rw [Pi.smul_apply, Pi.smul_apply, LinearMap.map_smul, hf hmn]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
x : M
hx : ∀ (n : ℕ), x ≡ 0 [SMOD ⊥ ^ n • ⊤]
⊢ x = 0
[PROOFSTEP]
simpa only [pow_one ⊥, bot_smul, SModEq.bot] using hx 1
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
h : IsHausdorff ⊤ M
x y : M
n : ℕ
⊢ x - y ≡ 0 [SMOD ⊤ ^ n • ⊤]
[PROOFSTEP]
rw [Ideal.top_pow, top_smul]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
h : IsHausdorff ⊤ M
x y : M
n : ℕ
⊢ x - y ≡ 0 [SMOD ⊤]
[PROOFSTEP]
exact SModEq.top
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
x✝ : Hausdorffification I M
x : M
hx : ∀ (n : ℕ), Quotient.mk'' x ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
⊢ x ∈ I ^ n • ⊤
[PROOFSTEP]
have := comap_map_mkQ (⨅ n : ℕ, I ^ n • ⊤ : Submodule R M) (I ^ n • ⊤)
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
x✝ : Hausdorffification I M
x : M
hx : ∀ (n : ℕ), Quotient.mk'' x ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
this :
  comap (mkQ (⨅ (n : ℕ), I ^ n • ⊤)) (map (mkQ (⨅ (n : ℕ), I ^ n • ⊤)) (I ^ n • ⊤)) = (⨅ (n : ℕ), I ^ n • ⊤) ⊔ I ^ n • ⊤
⊢ x ∈ I ^ n • ⊤
[PROOFSTEP]
simp only [sup_of_le_right (iInf_le (fun n => (I ^ n • ⊤ : Submodule R M)) n)] at this
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
x✝ : Hausdorffification I M
x : M
hx : ∀ (n : ℕ), Quotient.mk'' x ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
this : comap (mkQ (⨅ (n : ℕ), I ^ n • ⊤)) (map (mkQ (⨅ (n : ℕ), I ^ n • ⊤)) (I ^ n • ⊤)) = I ^ n • ⊤
⊢ x ∈ I ^ n • ⊤
[PROOFSTEP]
rw [← this, map_smul'', mem_comap, Submodule.map_top, range_mkQ, ← SModEq.zero]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
x✝ : Hausdorffification I M
x : M
hx : ∀ (n : ℕ), Quotient.mk'' x ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
this : comap (mkQ (⨅ (n : ℕ), I ^ n • ⊤)) (map (mkQ (⨅ (n : ℕ), I ^ n • ⊤)) (I ^ n • ⊤)) = I ^ n • ⊤
⊢ ↑(mkQ (⨅ (n : ℕ), I ^ n • ⊤)) x ≡ 0 [SMOD I ^ n • ⊤]
[PROOFSTEP]
exact hx n
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
h : IsHausdorff I N
f : M →ₗ[R] N
n : ℕ
⊢ map f (I ^ n • ⊤) ≤ I ^ n • ⊤
[PROOFSTEP]
rw [map_smul'']
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
h : IsHausdorff I N
f : M →ₗ[R] N
n : ℕ
⊢ I ^ n • map f ⊤ ≤ I ^ n • ⊤
[PROOFSTEP]
exact smul_mono le_rfl le_top
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
h : IsHausdorff I N
f : M →ₗ[R] N
g : Hausdorffification I M →ₗ[R] N
hg : LinearMap.comp g (of I M) = f
x✝ : Hausdorffification I M
x : M
⊢ ↑g (↑(of I M) x) = ↑(lift I f) (↑(of I M) x)
[PROOFSTEP]
rw [lift_of, ← hg, LinearMap.comp_apply]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ IsPrecomplete ⊥ M
[PROOFSTEP]
refine' ⟨fun f hf => ⟨f 1, fun n => _⟩⟩
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ℕ → M
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊥ ^ m • ⊤]
n : ℕ
⊢ f n ≡ f 1 [SMOD ⊥ ^ n • ⊤]
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ℕ → M
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊥ ^ m • ⊤]
⊢ f Nat.zero ≡ f 1 [SMOD ⊥ ^ Nat.zero • ⊤]
[PROOFSTEP]
rw [pow_zero, Ideal.one_eq_top, top_smul]
[GOAL]
case zero
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ℕ → M
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊥ ^ m • ⊤]
⊢ f Nat.zero ≡ f 1 [SMOD ⊤]
[PROOFSTEP]
exact SModEq.top
[GOAL]
case succ
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ℕ → M
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊥ ^ m • ⊤]
n : ℕ
⊢ f (Nat.succ n) ≡ f 1 [SMOD ⊥ ^ Nat.succ n • ⊤]
[PROOFSTEP]
specialize hf (Nat.le_add_left 1 n)
[GOAL]
case succ
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ℕ → M
n : ℕ
hf : f 1 ≡ f (n + 1) [SMOD ⊥ ^ 1 • ⊤]
⊢ f (Nat.succ n) ≡ f 1 [SMOD ⊥ ^ Nat.succ n • ⊤]
[PROOFSTEP]
rw [pow_one, bot_smul, SModEq.bot] at hf
[GOAL]
case succ
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ℕ → M
n : ℕ
hf : f 1 = f (n + 1)
⊢ f (Nat.succ n) ≡ f 1 [SMOD ⊥ ^ Nat.succ n • ⊤]
[PROOFSTEP]
rw [hf]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ℕ → M
x✝ : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊤ ^ m • ⊤]
n : ℕ
⊢ f n ≡ 0 [SMOD ⊤ ^ n • ⊤]
[PROOFSTEP]
rw [Ideal.top_pow, top_smul]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ℕ → M
x✝ : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊤ ^ m • ⊤]
n : ℕ
⊢ f n ≡ 0 [SMOD ⊤]
[PROOFSTEP]
exact SModEq.top
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Subsingleton M
f : ℕ → M
x✝ : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
n : ℕ
⊢ f n ≡ 0 [SMOD I ^ n • ⊤]
[PROOFSTEP]
rw [Subsingleton.elim (f n) 0]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
x : { x // x ∈ adicCompletion I M }
hx : ∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
x✝¹ x✝ : { x // x ∈ adicCompletion I M }
ih1 : ↑(eval I M n) x✝¹ = ↑(eval I M n) 0
ih2 : ↑(eval I M n) x✝ = ↑(eval I M n) 0
⊢ ↑(eval I M n) (x✝¹ + x✝) = ↑(eval I M n) 0
[PROOFSTEP]
rw [LinearMap.map_add, ih1, ih2, LinearMap.map_zero, add_zero]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
⊢ I ≤ Ideal.jacobson ⊥
[PROOFSTEP]
intro x hx
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
⊢ x ∈ Ideal.jacobson ⊥
[PROOFSTEP]
rw [← Ideal.neg_mem_iff, Ideal.mem_jacobson_bot]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
⊢ ∀ (y : R), IsUnit (-x * y + 1)
[PROOFSTEP]
intro y
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
⊢ IsUnit (-x * y + 1)
[PROOFSTEP]
rw [add_comm]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
⊢ IsUnit (1 + -x * y)
[PROOFSTEP]
let f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
⊢ IsUnit (1 + -x * y)
[PROOFSTEP]
have hf : ∀ m n, m ≤ n → f m ≡ f n [SMOD I ^ m • (⊤ : Submodule R R)] :=
  by
  intro m n h
  simp only [Algebra.id.smul_eq_mul, Ideal.mul_top, SModEq.sub_mem]
  rw [← add_tsub_cancel_of_le h, Finset.sum_range_add, ← sub_sub, sub_self, zero_sub, @neg_mem_iff]
  apply Submodule.sum_mem
  intro n _
  rw [mul_pow, pow_add, mul_assoc]
  exact Ideal.mul_mem_right _ (I ^ m) (Ideal.pow_mem_pow hx m)
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
⊢ ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
[PROOFSTEP]
intro m n h
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
m n : ℕ
h : m ≤ n
⊢ f m ≡ f n [SMOD I ^ m • ⊤]
[PROOFSTEP]
simp only [Algebra.id.smul_eq_mul, Ideal.mul_top, SModEq.sub_mem]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
m n : ℕ
h : m ≤ n
⊢ ∑ i in range m, (x * y) ^ i - ∑ i in range n, (x * y) ^ i ∈ I ^ m
[PROOFSTEP]
rw [← add_tsub_cancel_of_le h, Finset.sum_range_add, ← sub_sub, sub_self, zero_sub, @neg_mem_iff]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
m n : ℕ
h : m ≤ n
⊢ ∑ x_1 in range (n - m), (x * y) ^ (m + x_1) ∈ I ^ m
[PROOFSTEP]
apply Submodule.sum_mem
[GOAL]
case a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
m n : ℕ
h : m ≤ n
⊢ ∀ (c : ℕ), c ∈ range (n - m) → (x * y) ^ (m + c) ∈ I ^ m
[PROOFSTEP]
intro n _
[GOAL]
case a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
m n✝ : ℕ
h : m ≤ n✝
n : ℕ
a✝ : n ∈ range (n✝ - m)
⊢ (x * y) ^ (m + n) ∈ I ^ m
[PROOFSTEP]
rw [mul_pow, pow_add, mul_assoc]
[GOAL]
case a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
m n✝ : ℕ
h : m ≤ n✝
n : ℕ
a✝ : n ∈ range (n✝ - m)
⊢ x ^ m * (x ^ n * y ^ (m + n)) ∈ I ^ m
[PROOFSTEP]
exact Ideal.mul_mem_right _ (I ^ m) (Ideal.pow_mem_pow hx m)
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
⊢ IsUnit (1 + -x * y)
[PROOFSTEP]
obtain ⟨L, hL⟩ := IsPrecomplete.prec toIsPrecomplete @hf
[GOAL]
case intro
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
hL : ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]
⊢ IsUnit (1 + -x * y)
[PROOFSTEP]
rw [isUnit_iff_exists_inv]
[GOAL]
case intro
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
hL : ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]
⊢ ∃ b, (1 + -x * y) * b = 1
[PROOFSTEP]
use L
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
hL : ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]
⊢ (1 + -x * y) * L = 1
[PROOFSTEP]
rw [← sub_eq_zero, neg_mul]
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
hL : ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]
⊢ (1 + -(x * y)) * L - 1 = 0
[PROOFSTEP]
apply IsHausdorff.haus (toIsHausdorff : IsHausdorff I R)
[GOAL]
case h.a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
hL : ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]
⊢ ∀ (n : ℕ), (1 + -(x * y)) * L - 1 ≡ 0 [SMOD I ^ n • ⊤]
[PROOFSTEP]
intro n
[GOAL]
case h.a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
hL : ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]
n : ℕ
⊢ (1 + -(x * y)) * L - 1 ≡ 0 [SMOD I ^ n • ⊤]
[PROOFSTEP]
specialize hL n
[GOAL]
case h.a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n : ℕ
hL : f n ≡ L [SMOD I ^ n • ⊤]
⊢ (1 + -(x * y)) * L - 1 ≡ 0 [SMOD I ^ n • ⊤]
[PROOFSTEP]
rw [SModEq.sub_mem, Algebra.id.smul_eq_mul, Ideal.mul_top] at hL ⊢
[GOAL]
case h.a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n : ℕ
hL : f n - L ∈ I ^ n
⊢ (1 + -(x * y)) * L - 1 - 0 ∈ I ^ n
[PROOFSTEP]
rw [sub_zero]
[GOAL]
case h.a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n : ℕ
hL : f n - L ∈ I ^ n
⊢ (1 + -(x * y)) * L - 1 ∈ I ^ n
[PROOFSTEP]
suffices (1 - x * y) * f n - 1 ∈ I ^ n
  by
  convert Ideal.sub_mem _ this (Ideal.mul_mem_left _ (1 + -(x * y)) hL) using 1
  ring
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n : ℕ
hL : f n - L ∈ I ^ n
this : (1 - x * y) * f n - 1 ∈ I ^ n
⊢ (1 + -(x * y)) * L - 1 ∈ I ^ n
[PROOFSTEP]
convert Ideal.sub_mem _ this (Ideal.mul_mem_left _ (1 + -(x * y)) hL) using 1
[GOAL]
case h.e'_4
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n : ℕ
hL : f n - L ∈ I ^ n
this : (1 - x * y) * f n - 1 ∈ I ^ n
⊢ (1 + -(x * y)) * L - 1 = (1 - x * y) * f n - 1 - (1 + -(x * y)) * (f n - L)
[PROOFSTEP]
ring
[GOAL]
case h.a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n : ℕ
hL : f n - L ∈ I ^ n
⊢ (1 - x * y) * f n - 1 ∈ I ^ n
[PROOFSTEP]
cases n
[GOAL]
case h.a.zero
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
hL : f Nat.zero - L ∈ I ^ Nat.zero
⊢ (1 - x * y) * f Nat.zero - 1 ∈ I ^ Nat.zero
[PROOFSTEP]
simp only [Ideal.one_eq_top, pow_zero, Nat.zero_eq, mem_top]
[GOAL]
case h.a.succ
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n✝ : ℕ
hL : f (Nat.succ n✝) - L ∈ I ^ Nat.succ n✝
⊢ (1 - x * y) * f (Nat.succ n✝) - 1 ∈ I ^ Nat.succ n✝
[PROOFSTEP]
rw [← neg_sub _ (1 : R), neg_mul, mul_geom_sum, neg_sub, sub_sub, add_comm, ← sub_sub, sub_self, zero_sub, @neg_mem_iff,
  mul_pow]
[GOAL]
case h.a.succ
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n✝ : ℕ
hL : f (Nat.succ n✝) - L ∈ I ^ Nat.succ n✝
⊢ x ^ Nat.succ n✝ * y ^ Nat.succ n✝ ∈ I ^ Nat.succ n✝
[PROOFSTEP]
exact Ideal.mul_mem_right _ (I ^ _) (Ideal.pow_mem_pow hx _)


[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝ : AddGroup n
⊢ Injective circulant
[PROOFSTEP]
intro v w h
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝ : AddGroup n
v w : n → α
h : circulant v = circulant w
⊢ v = w
[PROOFSTEP]
ext k
[GOAL]
case h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝ : AddGroup n
v w : n → α
h : circulant v = circulant w
k : n
⊢ v k = w k
[PROOFSTEP]
rw [← circulant_col_zero_eq v, ← circulant_col_zero_eq w, h]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
⊢ Injective fun v => circulant v
[PROOFSTEP]
simp [Injective]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝ : AddGroup n
v : n → α
⊢ (circulant v)ᵀ = circulant fun i => v (-i)
[PROOFSTEP]
ext
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝ : AddGroup n
v : n → α
i✝ x✝ : n
⊢ (circulant v)ᵀ i✝ x✝ = circulant (fun i => v (-i)) i✝ x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝¹ : Star α
inst✝ : AddGroup n
v : n → α
⊢ (circulant v)ᴴ = circulant (star fun i => v (-i))
[PROOFSTEP]
ext
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝¹ : Star α
inst✝ : AddGroup n
v : n → α
i✝ x✝ : n
⊢ (circulant v)ᴴ i✝ x✝ = circulant (star fun i => v (-i)) i✝ x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
⊢ ∀ (v : Fin 0 → α), (circulant v)ᵀ = circulant fun i => v (-i)
[PROOFSTEP]
simp [Injective]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝ : Star α
⊢ ∀ (v : Fin 0 → α), (circulant v)ᴴ = circulant (star fun i => v (-i))
[PROOFSTEP]
simp [Injective]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
⊢ circulant v * circulant w = circulant (mulVec (circulant v) w)
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j : n
⊢ (circulant v * circulant w) i j = circulant (mulVec (circulant v) w) i j
[PROOFSTEP]
simp only [mul_apply, mulVec, circulant_apply, dotProduct]
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j : n
⊢ ∑ x : n, v (i - x) * w (x - j) = ∑ x : n, v (i - j - x) * w x
[PROOFSTEP]
refine' Fintype.sum_equiv (Equiv.subRight j) _ _ _
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j : n
⊢ ∀ (x : n), v (i - x) * w (x - j) = v (i - j - ↑(Equiv.subRight j) x) * w (↑(Equiv.subRight j) x)
[PROOFSTEP]
intro x
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝² : Semiring α
inst✝¹ : Fintype n
inst✝ : AddGroup n
v w : n → α
i j x : n
⊢ v (i - x) * w (x - j) = v (i - j - ↑(Equiv.subRight j) x) * w (↑(Equiv.subRight j) x)
[PROOFSTEP]
simp only [Equiv.subRight_apply, sub_sub_sub_cancel_right]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝ : Semiring α
⊢ ∀ (v w : Fin 0 → α), circulant v * circulant w = circulant (mulVec (circulant v) w)
[PROOFSTEP]
simp [Injective]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
⊢ circulant v * circulant w = circulant w * circulant v
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j : n
⊢ (circulant v * circulant w) i j = (circulant w * circulant v) i j
[PROOFSTEP]
simp only [mul_apply, circulant_apply, mul_comm]
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j : n
⊢ ∑ x : n, v (i - x) * w (x - j) = ∑ x : n, w (i - x) * v (x - j)
[PROOFSTEP]
refine' Fintype.sum_equiv ((Equiv.subLeft i).trans (Equiv.addRight j)) _ _ _
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j : n
⊢ ∀ (x : n),
    v (i - x) * w (x - j) =
      w (i - ↑((Equiv.subLeft i).trans (Equiv.addRight j)) x) * v (↑((Equiv.subLeft i).trans (Equiv.addRight j)) x - j)
[PROOFSTEP]
intro x
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j x : n
⊢ v (i - x) * w (x - j) =
    w (i - ↑((Equiv.subLeft i).trans (Equiv.addRight j)) x) * v (↑((Equiv.subLeft i).trans (Equiv.addRight j)) x - j)
[PROOFSTEP]
simp [mul_comm]
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j x : n
⊢ v (i - x) * w (x - j) = v (i - x) * w (i - (i - x + j))
[PROOFSTEP]
congr 2
[GOAL]
case a.h.e_a.e_a
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j x : n
⊢ x - j = i - (i - x + j)
[PROOFSTEP]
abel
[GOAL]
case a.h.e_a.e_a
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝³ : CommSemigroup α
inst✝² : AddCommMonoid α
inst✝¹ : Fintype n
inst✝ : AddCommGroup n
v w : n → α
i j x : n
⊢ x - j = i - (i - x + j)
[PROOFSTEP]
abel
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝¹ : CommSemigroup α
inst✝ : AddCommMonoid α
⊢ ∀ (v w : Fin 0 → α), circulant v * circulant w = circulant w * circulant v
[PROOFSTEP]
simp [Injective]
[GOAL]
α✝ : Type u_1
β : Type u_2
m : Type u_3
n✝ : Type u_4
R : Type u_5
α : Type u_6
n : Type u_7
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : DecidableEq n
inst✝ : AddGroup n
⊢ circulant (Pi.single 0 1) = 1
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α✝ : Type u_1
β : Type u_2
m : Type u_3
n✝ : Type u_4
R : Type u_5
α : Type u_6
n : Type u_7
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : DecidableEq n
inst✝ : AddGroup n
i j : n
⊢ circulant (Pi.single 0 1) i j = OfNat.ofNat 1 i j
[PROOFSTEP]
simp [one_apply, Pi.single_apply, sub_eq_zero]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n✝ : Type u_4
R : Type u_5
n : Type u_6
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : AddGroup n
inst✝ : Fintype n
a : α
⊢ circulant (Pi.single 0 a) = ↑(scalar n) a
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n✝ : Type u_4
R : Type u_5
n : Type u_6
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : AddGroup n
inst✝ : Fintype n
a : α
i j : n
⊢ circulant (Pi.single 0 a) i j = ↑(scalar n) a i j
[PROOFSTEP]
simp [Pi.single_apply, one_apply, sub_eq_zero]
[GOAL]
α✝ : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
α : Type u_6
inst✝¹ : Zero α
inst✝ : One α
⊢ (circulant fun i => if ↑i = 0 then 1 else 0) = 1
[PROOFSTEP]
simp [Injective]
[GOAL]
α✝ : Type u_1
β : Type u_2
m : Type u_3
n✝ : Type u_4
R : Type u_5
α : Type u_6
inst✝¹ : Zero α
inst✝ : One α
n : ℕ
⊢ (circulant fun i => if ↑i = 0 then 1 else 0) = 1
[PROOFSTEP]
rw [← circulant_single_one]
[GOAL]
α✝ : Type u_1
β : Type u_2
m : Type u_3
n✝ : Type u_4
R : Type u_5
α : Type u_6
inst✝¹ : Zero α
inst✝ : One α
n : ℕ
⊢ (circulant fun i => if ↑i = 0 then 1 else 0) = circulant (Pi.single 0 1)
[PROOFSTEP]
congr with j
[GOAL]
case a.h
α✝ : Type u_1
β : Type u_2
m : Type u_3
n✝ : Type u_4
R : Type u_5
α : Type u_6
inst✝¹ : Zero α
inst✝ : One α
n : ℕ
j x✝ : Fin (n + 1)
⊢ circulant (fun i => if ↑i = 0 then 1 else 0) j x✝ = circulant (Pi.single 0 1) j x✝
[PROOFSTEP]
simp [Pi.single_apply, Fin.ext_iff]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
inst✝ : AddGroup n
v : n → α
⊢ IsSymm (circulant v) ↔ ∀ (i : n), v (-i) = v i
[PROOFSTEP]
rw [IsSymm, transpose_circulant, circulant_inj, funext_iff]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
R : Type u_5
v✝ : Fin 0 → α
⊢ IsSymm (circulant v✝) ↔ ∀ (i : Fin 0), v✝ (-i) = v✝ i
[PROOFSTEP]
simp [IsSymm.ext_iff, IsEmpty.forall_iff]


[GOAL]
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : degree q = 1
⊢ eigenspace f (-coeff q 0 / leadingCoeff q) =
    LinearMap.ker (leadingCoeff q • f - ↑(algebraMap K (End K V)) (-coeff q 0))
[PROOFSTEP]
rw [eigenspace_div]
[GOAL]
case hb
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : degree q = 1
⊢ leadingCoeff q ≠ 0
[PROOFSTEP]
intro h
[GOAL]
case hb
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : degree q = 1
h : leadingCoeff q = 0
⊢ False
[PROOFSTEP]
rw [leadingCoeff_eq_zero_iff_deg_eq_bot.1 h] at hq
[GOAL]
case hb
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : ⊥ = 1
h : leadingCoeff q = 0
⊢ False
[PROOFSTEP]
cases hq
[GOAL]
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : degree q = 1
⊢ LinearMap.ker (leadingCoeff q • f - ↑(algebraMap K (End K V)) (-coeff q 0)) =
    LinearMap.ker (↑(aeval f) (↑C (leadingCoeff q) * X + ↑C (coeff q 0)))
[PROOFSTEP]
rw [C_mul', aeval_def]
[GOAL]
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : degree q = 1
⊢ LinearMap.ker (leadingCoeff q • f - ↑(algebraMap K (End K V)) (-coeff q 0)) =
    LinearMap.ker (eval₂ (algebraMap K (End K V)) f (leadingCoeff q • X + ↑C (coeff q 0)))
[PROOFSTEP]
simp [algebraMap, Algebra.toRingHom]
[GOAL]
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
q : K[X]
hq : degree q = 1
⊢ LinearMap.ker (↑(aeval f) (↑C (leadingCoeff q) * X + ↑C (coeff q 0))) = LinearMap.ker (↑(aeval f) q)
[PROOFSTEP]
rwa [← eq_X_add_C_of_degree_eq_one]
[GOAL]
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
c : K[X]ˣ
⊢ LinearMap.ker (↑(aeval f) ↑c) = ⊥
[PROOFSTEP]
rw [Polynomial.eq_C_of_degree_eq_zero (degree_coe_units c)]
[GOAL]
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
c : K[X]ˣ
⊢ LinearMap.ker (↑(aeval f) (↑C (coeff (↑c) 0))) = ⊥
[PROOFSTEP]
simp only [aeval_def, eval₂_C]
[GOAL]
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
c : K[X]ˣ
⊢ LinearMap.ker (↑(algebraMap K (End K V)) (coeff (↑c) 0)) = ⊥
[PROOFSTEP]
apply ker_algebraMap_end
[GOAL]
case ha
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
c : K[X]ˣ
⊢ coeff (↑c) 0 ≠ 0
[PROOFSTEP]
apply coeff_coe_units_zero_ne_zero c
[GOAL]
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : HasEigenvector f μ x
⊢ ↑(↑(aeval f) p) x = eval μ p • x
[PROOFSTEP]
refine' p.induction_on _ _ _
[GOAL]
case refine'_1
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : HasEigenvector f μ x
⊢ ∀ (a : K), ↑(↑(aeval f) (↑C a)) x = eval μ (↑C a) • x
[PROOFSTEP]
intro a
[GOAL]
case refine'_1
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : HasEigenvector f μ x
a : K
⊢ ↑(↑(aeval f) (↑C a)) x = eval μ (↑C a) • x
[PROOFSTEP]
simp [Module.algebraMap_end_apply]
[GOAL]
case refine'_2
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : HasEigenvector f μ x
⊢ ∀ (p q : K[X]),
    ↑(↑(aeval f) p) x = eval μ p • x → ↑(↑(aeval f) q) x = eval μ q • x → ↑(↑(aeval f) (p + q)) x = eval μ (p + q) • x
[PROOFSTEP]
intro p q hp hq
[GOAL]
case refine'_2
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p✝ : K[X]
μ : K
x : V
h : HasEigenvector f μ x
p q : K[X]
hp : ↑(↑(aeval f) p) x = eval μ p • x
hq : ↑(↑(aeval f) q) x = eval μ q • x
⊢ ↑(↑(aeval f) (p + q)) x = eval μ (p + q) • x
[PROOFSTEP]
simp [hp, hq, add_smul]
[GOAL]
case refine'_3
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : HasEigenvector f μ x
⊢ ∀ (n : ℕ) (a : K),
    ↑(↑(aeval f) (↑C a * X ^ n)) x = eval μ (↑C a * X ^ n) • x →
      ↑(↑(aeval f) (↑C a * X ^ (n + 1))) x = eval μ (↑C a * X ^ (n + 1)) • x
[PROOFSTEP]
intro n a hna
[GOAL]
case refine'_3
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : HasEigenvector f μ x
n : ℕ
a : K
hna : ↑(↑(aeval f) (↑C a * X ^ n)) x = eval μ (↑C a * X ^ n) • x
⊢ ↑(↑(aeval f) (↑C a * X ^ (n + 1))) x = eval μ (↑C a * X ^ (n + 1)) • x
[PROOFSTEP]
rw [mul_comm, pow_succ, mul_assoc, AlgHom.map_mul, LinearMap.mul_apply, mul_comm, hna]
[GOAL]
case refine'_3
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
p : K[X]
μ : K
x : V
h : HasEigenvector f μ x
n : ℕ
a : K
hna : ↑(↑(aeval f) (↑C a * X ^ n)) x = eval μ (↑C a * X ^ n) • x
⊢ ↑(↑(aeval f) X) (eval μ (↑C a * X ^ n) • x) = eval μ (X * (↑C a * X ^ n)) • x
[PROOFSTEP]
simp only [mem_eigenspace_iff.1 h.1, smul_smul, aeval_X, eval_mul, eval_C, eval_pow, eval_X, LinearMap.map_smulₛₗ,
  RingHom.id_apply, mul_comm]
[GOAL]
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
h : HasEigenvalue f μ
⊢ IsRoot (minpoly K f) μ
[PROOFSTEP]
rcases(Submodule.ne_bot_iff _).1 h with ⟨w, ⟨H, ne0⟩⟩
[GOAL]
case intro.intro
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
h : HasEigenvalue f μ
w : V
H : w ∈ eigenspace f μ
ne0 : w ≠ 0
⊢ IsRoot (minpoly K f) μ
[PROOFSTEP]
refine' Or.resolve_right (smul_eq_zero.1 _) ne0
[GOAL]
case intro.intro
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
h : HasEigenvalue f μ
w : V
H : w ∈ eigenspace f μ
ne0 : w ≠ 0
⊢ eval μ (minpoly K f) • w = 0
[PROOFSTEP]
simp [← aeval_apply_of_hasEigenvector ⟨H, ne0⟩, minpoly.aeval K f]
[GOAL]
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
⊢ HasEigenvalue f μ
[PROOFSTEP]
cases' dvd_iff_isRoot.2 h with p hp
[GOAL]
case intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
⊢ HasEigenvalue f μ
[PROOFSTEP]
rw [HasEigenvalue, eigenspace]
[GOAL]
case intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
⊢ LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) ≠ ⊥
[PROOFSTEP]
intro con
[GOAL]
case intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
con : LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) = ⊥
⊢ False
[PROOFSTEP]
cases' (LinearMap.isUnit_iff_ker_eq_bot _).2 con with u hu
[GOAL]
case intro.intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
con : LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - ↑(algebraMap K (End K V)) μ
⊢ False
[PROOFSTEP]
have p_ne_0 : p ≠ 0 := by
  intro con
  apply minpoly.ne_zero f.isIntegral
  rw [hp, con, mul_zero]
[GOAL]
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
con : LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - ↑(algebraMap K (End K V)) μ
⊢ p ≠ 0
[PROOFSTEP]
intro con
[GOAL]
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
con✝ : LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - ↑(algebraMap K (End K V)) μ
con : p = 0
⊢ False
[PROOFSTEP]
apply minpoly.ne_zero f.isIntegral
[GOAL]
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
con✝ : LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - ↑(algebraMap K (End K V)) μ
con : p = 0
⊢ minpoly K f = 0
[PROOFSTEP]
rw [hp, con, mul_zero]
[GOAL]
case intro.intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
con : LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - ↑(algebraMap K (End K V)) μ
p_ne_0 : p ≠ 0
⊢ False
[PROOFSTEP]
have : (aeval f) p = 0 := by
  have h_aeval := minpoly.aeval K f
  revert h_aeval
  simp [hp, ← hu]
[GOAL]
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
con : LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - ↑(algebraMap K (End K V)) μ
p_ne_0 : p ≠ 0
⊢ ↑(aeval f) p = 0
[PROOFSTEP]
have h_aeval := minpoly.aeval K f
[GOAL]
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
con : LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - ↑(algebraMap K (End K V)) μ
p_ne_0 : p ≠ 0
h_aeval : ↑(aeval f) (minpoly K f) = 0
⊢ ↑(aeval f) p = 0
[PROOFSTEP]
revert h_aeval
[GOAL]
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
con : LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - ↑(algebraMap K (End K V)) μ
p_ne_0 : p ≠ 0
⊢ ↑(aeval f) (minpoly K f) = 0 → ↑(aeval f) p = 0
[PROOFSTEP]
simp [hp, ← hu]
[GOAL]
case intro.intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
con : LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - ↑(algebraMap K (End K V)) μ
p_ne_0 : p ≠ 0
this : ↑(aeval f) p = 0
⊢ False
[PROOFSTEP]
have h_deg := minpoly.degree_le_of_ne_zero K f p_ne_0 this
[GOAL]
case intro.intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
con : LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - ↑(algebraMap K (End K V)) μ
p_ne_0 : p ≠ 0
this : ↑(aeval f) p = 0
h_deg : degree (minpoly K f) ≤ degree p
⊢ False
[PROOFSTEP]
rw [hp, degree_mul, degree_X_sub_C, Polynomial.degree_eq_natDegree p_ne_0] at h_deg
[GOAL]
case intro.intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
con : LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - ↑(algebraMap K (End K V)) μ
p_ne_0 : p ≠ 0
this : ↑(aeval f) p = 0
h_deg : 1 + ↑(natDegree p) ≤ ↑(natDegree p)
⊢ False
[PROOFSTEP]
norm_cast at h_deg
[GOAL]
case intro.intro
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
h : IsRoot (minpoly K f) μ
p : K[X]
hp : minpoly K f = (X - ↑C μ) * p
con : LinearMap.ker (f - ↑(algebraMap K (End K V)) μ) = ⊥
u : (V →ₗ[K] V)ˣ
hu : ↑u = f - ↑(algebraMap K (End K V)) μ
p_ne_0 : p ≠ 0
this : ↑(aeval f) p = 0
h_deg : 1 + natDegree p ≤ natDegree p
⊢ False
[PROOFSTEP]
linarith
[GOAL]
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f✝ : End K V
μ : K
f : End K V
⊢ Set.Finite {μ | eigenspace f μ ≠ ⊥}
[PROOFSTEP]
have h : minpoly K f ≠ 0 := minpoly.ne_zero f.isIntegral
[GOAL]
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f✝ : End K V
μ : K
f : End K V
h : minpoly K f ≠ 0
⊢ Set.Finite {μ | eigenspace f μ ≠ ⊥}
[PROOFSTEP]
convert (minpoly K f).rootSet_finite K
[GOAL]
case h.e'_2
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f✝ : End K V
μ : K
f : End K V
h : minpoly K f ≠ 0
⊢ {μ | eigenspace f μ ≠ ⊥} = rootSet (minpoly K f) K
[PROOFSTEP]
ext μ
[GOAL]
case h.e'_2.h
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f✝ : End K V
μ✝ : K
f : End K V
h : minpoly K f ≠ 0
μ : K
⊢ μ ∈ {μ | eigenspace f μ ≠ ⊥} ↔ μ ∈ rootSet (minpoly K f) K
[PROOFSTEP]
rw [Set.mem_setOf_eq, ← HasEigenvalue, hasEigenvalue_iff_isRoot, mem_rootSet_of_ne h, IsRoot, coe_aeval_eq_eval]


[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosDef M
⊢ PosSemidef M
[PROOFSTEP]
refine' ⟨hM.1, _⟩
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosDef M
⊢ ∀ (x : n → R), 0 ≤ star x ⬝ᵥ mulVec M x
[PROOFSTEP]
intro x
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosDef M
x : n → R
⊢ 0 ≤ star x ⬝ᵥ mulVec M x
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosDef M
x : n → R
hx : x = 0
⊢ 0 ≤ star x ⬝ᵥ mulVec M x
[PROOFSTEP]
simp only [hx, zero_dotProduct, star_zero, IsROrC.zero_re']
[GOAL]
case pos
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosDef M
x : n → R
hx : x = 0
⊢ 0 ≤ 0
[PROOFSTEP]
exact le_rfl
[GOAL]
case neg
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosDef M
x : n → R
hx : ¬x = 0
⊢ 0 ≤ star x ⬝ᵥ mulVec M x
[PROOFSTEP]
exact le_of_lt (hM.2 x hx)
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
⊢ PosSemidef (Matrix.submatrix M ↑e ↑e)
[PROOFSTEP]
refine' ⟨hM.1.submatrix e, fun x => _⟩
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
⊢ 0 ≤ star x ⬝ᵥ mulVec (Matrix.submatrix M ↑e ↑e) x
[PROOFSTEP]
have : (M.submatrix (⇑e) e).mulVec x = (M.mulVec fun i : n => x (e.symm i)) ∘ e :=
  by
  ext i
  dsimp only [(· ∘ ·), mulVec, dotProduct]
  rw [Finset.sum_bij' (fun i _ => e i) _ _ fun i _ => e.symm i] <;>
    simp only [eq_self_iff_true, imp_true_iff, Equiv.symm_apply_apply, Finset.mem_univ, submatrix_apply,
      Equiv.apply_symm_apply]
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
⊢ mulVec (Matrix.submatrix M ↑e ↑e) x = (mulVec M fun i => x (↑e.symm i)) ∘ ↑e
[PROOFSTEP]
ext i
[GOAL]
case h
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
i : m
⊢ mulVec (Matrix.submatrix M ↑e ↑e) x i = ((mulVec M fun i => x (↑e.symm i)) ∘ ↑e) i
[PROOFSTEP]
dsimp only [(· ∘ ·), mulVec, dotProduct]
[GOAL]
case h
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
i : m
⊢ (Finset.sum Finset.univ fun i_1 => Matrix.submatrix M (↑e) (↑e) i i_1 * x i_1) =
    Finset.sum Finset.univ fun i_1 => M (↑e i) i_1 * x (↑e.symm i_1)
[PROOFSTEP]
rw [Finset.sum_bij' (fun i _ => e i) _ _ fun i _ => e.symm i]
[GOAL]
case h.hj
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
i : m
⊢ ∀ (a : n), a ∈ Finset.univ → ↑e.symm a ∈ Finset.univ
[PROOFSTEP]
simp only [eq_self_iff_true, imp_true_iff, Equiv.symm_apply_apply, Finset.mem_univ, submatrix_apply,
  Equiv.apply_symm_apply]
[GOAL]
case h.left_inv
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
i : m
⊢ ∀ (a : m), a ∈ Finset.univ → ↑e.symm (↑e a) = a
[PROOFSTEP]
simp only [eq_self_iff_true, imp_true_iff, Equiv.symm_apply_apply, Finset.mem_univ, submatrix_apply,
  Equiv.apply_symm_apply]
[GOAL]
case h.right_inv
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
i : m
⊢ ∀ (a : n), a ∈ Finset.univ → ↑e (↑e.symm a) = a
[PROOFSTEP]
simp only [eq_self_iff_true, imp_true_iff, Equiv.symm_apply_apply, Finset.mem_univ, submatrix_apply,
  Equiv.apply_symm_apply]
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
i : m
⊢ ∀ (a : m) (ha : a ∈ Finset.univ), (fun i x => ↑e i) a ha ∈ Finset.univ
[PROOFSTEP]
simp only [eq_self_iff_true, imp_true_iff, Equiv.symm_apply_apply, Finset.mem_univ, submatrix_apply,
  Equiv.apply_symm_apply]
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
i : m
⊢ ∀ (a : m) (ha : a ∈ Finset.univ),
    Matrix.submatrix M (↑e) (↑e) i a * x a = M (↑e i) ((fun i x => ↑e i) a ha) * x (↑e.symm ((fun i x => ↑e i) a ha))
[PROOFSTEP]
simp only [eq_self_iff_true, imp_true_iff, Equiv.symm_apply_apply, Finset.mem_univ, submatrix_apply,
  Equiv.apply_symm_apply]
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
this : mulVec (Matrix.submatrix M ↑e ↑e) x = (mulVec M fun i => x (↑e.symm i)) ∘ ↑e
⊢ 0 ≤ star x ⬝ᵥ mulVec (Matrix.submatrix M ↑e ↑e) x
[PROOFSTEP]
rw [this]
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
this : mulVec (Matrix.submatrix M ↑e ↑e) x = (mulVec M fun i => x (↑e.symm i)) ∘ ↑e
⊢ 0 ≤ star x ⬝ᵥ (mulVec M fun i => x (↑e.symm i)) ∘ ↑e
[PROOFSTEP]
convert hM.2 fun i => x (e.symm i) using 3
[GOAL]
case h.e'_4
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
this : mulVec (Matrix.submatrix M ↑e ↑e) x = (mulVec M fun i => x (↑e.symm i)) ∘ ↑e
⊢ star x ⬝ᵥ (mulVec M fun i => x (↑e.symm i)) ∘ ↑e = (star fun i => x (↑e.symm i)) ⬝ᵥ mulVec M fun i => x (↑e.symm i)
[PROOFSTEP]
unfold dotProduct
[GOAL]
case h.e'_4
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
this : mulVec (Matrix.submatrix M ↑e ↑e) x = (mulVec M fun i => x (↑e.symm i)) ∘ ↑e
⊢ (Finset.sum Finset.univ fun i => star x i * ((mulVec M fun i => x (↑e.symm i)) ∘ ↑e) i) =
    Finset.sum Finset.univ fun i => star (fun i => x (↑e.symm i)) i * mulVec M (fun i => x (↑e.symm i)) i
[PROOFSTEP]
rw [Finset.sum_bij' (fun i _ => e i) _ _ fun i _ => e.symm i]
[GOAL]
case h.e'_4.hj
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
this : mulVec (Matrix.submatrix M ↑e ↑e) x = (mulVec M fun i => x (↑e.symm i)) ∘ ↑e
⊢ ∀ (a : n), a ∈ Finset.univ → ↑e.symm a ∈ Finset.univ
[PROOFSTEP]
simp
[GOAL]
case h.e'_4.left_inv
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
this : mulVec (Matrix.submatrix M ↑e ↑e) x = (mulVec M fun i => x (↑e.symm i)) ∘ ↑e
⊢ ∀ (a : m), a ∈ Finset.univ → ↑e.symm (↑e a) = a
[PROOFSTEP]
simp
[GOAL]
case h.e'_4.right_inv
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
this : mulVec (Matrix.submatrix M ↑e ↑e) x = (mulVec M fun i => x (↑e.symm i)) ∘ ↑e
⊢ ∀ (a : n), a ∈ Finset.univ → ↑e (↑e.symm a) = a
[PROOFSTEP]
simp
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
this : mulVec (Matrix.submatrix M ↑e ↑e) x = (mulVec M fun i => x (↑e.symm i)) ∘ ↑e
⊢ ∀ (a : m) (ha : a ∈ Finset.univ), (fun i x => ↑e i) a ha ∈ Finset.univ
[PROOFSTEP]
simp
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosSemidef M
e : m ≃ n
x : m → R
this : mulVec (Matrix.submatrix M ↑e ↑e) x = (mulVec M fun i => x (↑e.symm i)) ∘ ↑e
⊢ ∀ (a : m) (ha : a ∈ Finset.univ),
    star x a * ((mulVec M fun i => x (↑e.symm i)) ∘ ↑e) a =
      star (fun i => x (↑e.symm i)) ((fun i x => ↑e i) a ha) *
        mulVec M (fun i => x (↑e.symm i)) ((fun i x => ↑e i) a ha)
[PROOFSTEP]
simp
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
e : m ≃ n
h : PosSemidef (submatrix M ↑e ↑e)
⊢ PosSemidef M
[PROOFSTEP]
simpa using h.submatrix e.symm
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosDef M
⊢ PosDef Mᵀ
[PROOFSTEP]
refine ⟨IsHermitian.transpose hM.1, fun x hx => ?_⟩
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosDef M
x : n → R
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ mulVec Mᵀ x
[PROOFSTEP]
convert hM.2 (star x) (star_ne_zero.2 hx) using 1
[GOAL]
case h.e'_4
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
M : Matrix n n R
hM : PosDef M
x : n → R
hx : x ≠ 0
⊢ star x ⬝ᵥ mulVec Mᵀ x = star (star x) ⬝ᵥ mulVec M (star x)
[PROOFSTEP]
rw [mulVec_transpose, Matrix.dotProduct_mulVec, star_star, dotProduct_comm]
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarOrderedRing R
inst✝¹ : IsROrC 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : IsSymm M
hMq : QuadraticForm.PosDef (toQuadraticForm' M)
⊢ PosDef M
[PROOFSTEP]
refine' ⟨hM, fun x hx => _⟩
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarOrderedRing R
inst✝¹ : IsROrC 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : IsSymm M
hMq : QuadraticForm.PosDef (toQuadraticForm' M)
x : n → ℝ
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ mulVec M x
[PROOFSTEP]
simp only [toQuadraticForm', QuadraticForm.PosDef, BilinForm.toQuadraticForm_apply, Matrix.toBilin'_apply'] at hMq
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarOrderedRing R
inst✝¹ : IsROrC 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : IsSymm M
x : n → ℝ
hx : x ≠ 0
hMq : ∀ (x : n → ℝ), x ≠ 0 → 0 < x ⬝ᵥ mulVec M x
⊢ 0 < star x ⬝ᵥ mulVec M x
[PROOFSTEP]
apply hMq x hx
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarOrderedRing R
inst✝¹ : IsROrC 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : PosDef M
⊢ QuadraticForm.PosDef (toQuadraticForm' M)
[PROOFSTEP]
intro x hx
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarOrderedRing R
inst✝¹ : IsROrC 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : PosDef M
x : n → ℝ
hx : x ≠ 0
⊢ 0 < ↑(toQuadraticForm' M) x
[PROOFSTEP]
simp only [toQuadraticForm', BilinForm.toQuadraticForm_apply, Matrix.toBilin'_apply']
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarOrderedRing R
inst✝¹ : IsROrC 𝕜
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : PosDef M
x : n → ℝ
hx : x ≠ 0
⊢ 0 < x ⬝ᵥ mulVec M x
[PROOFSTEP]
apply hM.2 x hx
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
A : Matrix m n R
⊢ PosSemidef (Aᴴ * A)
[PROOFSTEP]
refine ⟨isHermitian_transpose_mul_self _, fun x => ?_⟩
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
A : Matrix m n R
x : n → R
⊢ 0 ≤ star x ⬝ᵥ mulVec (Aᴴ * A) x
[PROOFSTEP]
rw [← mulVec_mulVec, dotProduct_mulVec, vecMul_conjTranspose, star_star]
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
A : Matrix m n R
x : n → R
⊢ 0 ≤ star (mulVec A x) ⬝ᵥ mulVec A x
[PROOFSTEP]
exact Finset.sum_nonneg fun i _ => star_mul_self_nonneg _
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarOrderedRing R
inst✝ : IsROrC 𝕜
A : Matrix m n R
⊢ PosSemidef (A * Aᴴ)
[PROOFSTEP]
simpa only [conjTranspose_conjTranspose] using posSemidef_conjTranspose_mul_self Aᴴ
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarOrderedRing R
inst✝² : IsROrC 𝕜
inst✝¹ : DecidableEq n
inst✝ : DecidableEq 𝕜
A : Matrix n n 𝕜
hA : PosDef A
i : n
⊢ 0 < IsHermitian.eigenvalues (_ : IsHermitian A) i
[PROOFSTEP]
rw [hA.1.eigenvalues_eq, hA.1.transpose_eigenvectorMatrix_apply]
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarOrderedRing R
inst✝² : IsROrC 𝕜
inst✝¹ : DecidableEq n
inst✝ : DecidableEq 𝕜
A : Matrix n n 𝕜
hA : PosDef A
i : n
⊢ 0 <
    ↑IsROrC.re
      (star (↑(IsHermitian.eigenvectorBasis (_ : IsHermitian A)) i) ⬝ᵥ
        mulVec A (↑(IsHermitian.eigenvectorBasis (_ : IsHermitian A)) i))
[PROOFSTEP]
exact hA.re_dotProduct_pos <| hA.1.eigenvectorBasis.orthonormal.ne_zero i
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarOrderedRing R
inst✝¹ : IsROrC 𝕜
M : Matrix n n ℝ
hM : PosDef M
inst✝ : DecidableEq n
⊢ 0 < det M
[PROOFSTEP]
rw [hM.isHermitian.det_eq_prod_eigenvalues]
[GOAL]
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarOrderedRing R
inst✝¹ : IsROrC 𝕜
M : Matrix n n ℝ
hM : PosDef M
inst✝ : DecidableEq n
⊢ 0 < Finset.prod Finset.univ fun i => ↑(IsHermitian.eigenvalues (_ : IsHermitian M) i)
[PROOFSTEP]
apply Finset.prod_pos
[GOAL]
case h0
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarOrderedRing R
inst✝¹ : IsROrC 𝕜
M : Matrix n n ℝ
hM : PosDef M
inst✝ : DecidableEq n
⊢ ∀ (i : n), i ∈ Finset.univ → 0 < ↑(IsHermitian.eigenvalues (_ : IsHermitian M) i)
[PROOFSTEP]
intro i _
[GOAL]
case h0
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarOrderedRing R
inst✝¹ : IsROrC 𝕜
M : Matrix n n ℝ
hM : PosDef M
inst✝ : DecidableEq n
i : n
a✝ : i ∈ Finset.univ
⊢ 0 < ↑(IsHermitian.eigenvalues (_ : IsHermitian M) i)
[PROOFSTEP]
rw [hM.isHermitian.eigenvalues_eq]
[GOAL]
case h0
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarOrderedRing R
inst✝¹ : IsROrC 𝕜
M : Matrix n n ℝ
hM : PosDef M
inst✝ : DecidableEq n
i : n
a✝ : i ∈ Finset.univ
⊢ 0 <
    ↑(↑IsROrC.re
        (star ((IsHermitian.eigenvectorMatrix (_ : IsHermitian M))ᵀ i) ⬝ᵥ
          mulVec M ((IsHermitian.eigenvectorMatrix (_ : IsHermitian M))ᵀ i)))
[PROOFSTEP]
refine hM.2 _ fun h => ?_
[GOAL]
case h0
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarOrderedRing R
inst✝¹ : IsROrC 𝕜
M : Matrix n n ℝ
hM : PosDef M
inst✝ : DecidableEq n
i : n
a✝ : i ∈ Finset.univ
h : (IsHermitian.eigenvectorMatrix (_ : IsHermitian M))ᵀ i = 0
⊢ False
[PROOFSTEP]
have h_det : hM.isHermitian.eigenvectorMatrixᵀ.det = 0 := Matrix.det_eq_zero_of_row_eq_zero i fun j => congr_fun h j
[GOAL]
case h0
m : Type u_1
n : Type u_2
R : Type u_3
𝕜 : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarOrderedRing R
inst✝¹ : IsROrC 𝕜
M : Matrix n n ℝ
hM : PosDef M
inst✝ : DecidableEq n
i : n
a✝ : i ∈ Finset.univ
h : (IsHermitian.eigenvectorMatrix (_ : IsHermitian M))ᵀ i = 0
h_det : det (IsHermitian.eigenvectorMatrix (_ : IsHermitian M))ᵀ = 0
⊢ False
[PROOFSTEP]
simpa only [h_det, not_isUnit_zero] using isUnit_det_of_invertible hM.isHermitian.eigenvectorMatrixᵀ
[GOAL]
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ : Matrix.PosDef (toMatrix' Q)
⊢ PosDef Q
[PROOFSTEP]
rw [← toQuadraticForm_associated ℝ Q, ← BilinForm.toMatrix'.left_inv ((associatedHom ℝ) Q)]
[GOAL]
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ : Matrix.PosDef (toMatrix' Q)
⊢ PosDef
    (BilinForm.toQuadraticForm
      (LinearEquiv.invFun BilinForm.toMatrix' (AddHom.toFun (↑BilinForm.toMatrix').toAddHom (↑(associatedHom ℝ) Q))))
[PROOFSTEP]
apply Matrix.posDef_toQuadraticForm' hQ
[GOAL]
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ : PosDef Q
⊢ Matrix.PosDef (toMatrix' Q)
[PROOFSTEP]
rw [← toQuadraticForm_associated ℝ Q, ← BilinForm.toMatrix'.left_inv ((associatedHom ℝ) Q)] at hQ
[GOAL]
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ :
  PosDef
    (BilinForm.toQuadraticForm
      (LinearEquiv.invFun BilinForm.toMatrix' (AddHom.toFun (↑BilinForm.toMatrix').toAddHom (↑(associatedHom ℝ) Q))))
⊢ Matrix.PosDef (toMatrix' Q)
[PROOFSTEP]
apply Matrix.posDef_of_toQuadraticForm' (isSymm_toMatrix' Q) hQ
[GOAL]
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
n : Type u_2
inst✝ : Fintype n
M : Matrix n n 𝕜
hM : PosDef M
x y : n → 𝕜
⊢ ↑(starRingEnd 𝕜) (inner y x) = inner x y
[PROOFSTEP]
dsimp only [Inner.inner]
[GOAL]
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
n : Type u_2
inst✝ : Fintype n
M : Matrix n n 𝕜
hM : PosDef M
x y : n → 𝕜
⊢ ↑(starRingEnd 𝕜) (star y ⬝ᵥ mulVec M x) = star x ⬝ᵥ mulVec M y
[PROOFSTEP]
rw [star_dotProduct, starRingEnd_apply, star_star, star_mulVec, dotProduct_mulVec, hM.isHermitian.eq]
[GOAL]
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
n : Type u_2
inst✝ : Fintype n
M : Matrix n n 𝕜
hM : PosDef M
x : n → 𝕜
⊢ 0 ≤ ↑IsROrC.re (inner x x)
[PROOFSTEP]
by_cases h : x = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
n : Type u_2
inst✝ : Fintype n
M : Matrix n n 𝕜
hM : PosDef M
x : n → 𝕜
h : x = 0
⊢ 0 ≤ ↑IsROrC.re (inner x x)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
n : Type u_2
inst✝ : Fintype n
M : Matrix n n 𝕜
hM : PosDef M
x : n → 𝕜
h : ¬x = 0
⊢ 0 ≤ ↑IsROrC.re (inner x x)
[PROOFSTEP]
exact le_of_lt (hM.re_dotProduct_pos h)
[GOAL]
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
n : Type u_2
inst✝ : Fintype n
M : Matrix n n 𝕜
hM : PosDef M
x : n → 𝕜
hx : star x ⬝ᵥ mulVec M x = 0
⊢ x = 0
[PROOFSTEP]
by_contra' h
[GOAL]
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
n : Type u_2
inst✝ : Fintype n
M : Matrix n n 𝕜
hM : PosDef M
x : n → 𝕜
hx : star x ⬝ᵥ mulVec M x = 0
h : x ≠ 0
⊢ False
[PROOFSTEP]
simpa [hx, lt_irrefl] using hM.re_dotProduct_pos h
[GOAL]
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
n : Type u_2
inst✝ : Fintype n
M : Matrix n n 𝕜
hM : PosDef M
⊢ ∀ (x y z : n → 𝕜), inner (x + y) z = inner x z + inner y z
[PROOFSTEP]
simp only [star_add, add_dotProduct, eq_self_iff_true, forall_const]
[GOAL]
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
n : Type u_2
inst✝ : Fintype n
M : Matrix n n 𝕜
hM : PosDef M
x y : n → 𝕜
r : 𝕜
⊢ inner (r • x) y = ↑(starRingEnd 𝕜) r * inner x y
[PROOFSTEP]
simp only
[GOAL]
𝕜 : Type u_1
inst✝¹ : IsROrC 𝕜
n : Type u_2
inst✝ : Fintype n
M : Matrix n n 𝕜
hM : PosDef M
x y : n → 𝕜
r : 𝕜
⊢ star (r • x) ⬝ᵥ mulVec M y = ↑(starRingEnd 𝕜) r * star x ⬝ᵥ mulVec M y
[PROOFSTEP]
rw [← smul_eq_mul, ← smul_dotProduct, starRingEnd_apply, ← star_smul]