Physlib Documentation

QuantumInfo.ForMathlib.HermitianMat.NonSingular

theorem Matrix.isUnit_smul {d : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype d] [DecidableEq d] [CommSemiring R] [Semiring S] [Algebra R S] {c : R} (hA : IsUnit c) {M : Matrix d d S} (hM : IsUnit M) :

IsUnit (c • M)

theorem Matrix.isUnit_natCast {d : Type u_1} {F : Type u_4} [Fintype d] [DecidableEq d] [Field F] {n : ℕ} (hn : n ≠ 0) [CharZero F] :

theorem Matrix.isUnit_real_smul {d : Type u_1} {𝕜 : Type u_5} [Fintype d] [DecidableEq d] [RCLike 𝕜] {r : ℝ} (hr : r ≠ 0) {M : Matrix d d 𝕜} (hM : IsUnit M) :

IsUnit (r • M)

theorem Matrix.isUnit_real_cast {d : Type u_1} {𝕜 : Type u_5} [Fintype d] [DecidableEq d] [RCLike 𝕜] {r : ℝ} (hr : r ≠ 0) :

IsUnit (r • 1)

class HermitianMat.NonSingular {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommRing R] [StarRing R] (A : HermitianMat n R) :

isUnit : IsUnit ↑A

Instances

@[simp]

theorem HermitianMat.isUnit_mat_of_nonSingular {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommRing R] [StarRing R] (A : HermitianMat n R) [A.NonSingular] :

theorem HermitianMat.nonsingular_iff_isUnit {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommRing R] [StarRing R] (A : HermitianMat n R) :

A.NonSingular ↔ IsUnit ↑A

instance HermitianMat.instHasInv_of_invertible {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommRing R] [StarRing R] (A : HermitianMat n R) [i : Invertible ↑A] :

instance HermitianMat.instInvertible_of_hasInv {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommRing R] [StarRing R] (A : HermitianMat n R) [h : A.NonSingular] :

Invertible ↑A

Equations

A.instInvertible_of_hasInv = ⋯.invertible

instance HermitianMat.instNonSingularOfNat {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommRing R] [StarRing R] :

theorem HermitianMat.nonSingular_of_posDef {n : Type u_1} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A : HermitianMat n 𝕜} (hA : (↑A).PosDef) :

theorem HermitianMat.nonSingular_iff_posDef_of_PSD {n : Type u_1} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A : HermitianMat n 𝕜} (hA : 0 ≤ A) :

A.NonSingular ↔ (↑A).PosDef

theorem HermitianMat.nonSingular_smul {n : Type u_1} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A : HermitianMat n 𝕜} [i : A.NonSingular] {c : ℝ} (hc : IsUnit c) :

(c • A).NonSingular

theorem HermitianMat.nonSingular_iff_zero_notMem_spectrum {n : Type u_1} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A : HermitianMat n 𝕜} :

A.NonSingular ↔ 0 ∉ spectrum ℝ ↑A

theorem HermitianMat.nonSingular_iff_eigenvalue_ne_zero {n : Type u_1} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A : HermitianMat n 𝕜} :

A.NonSingular ↔ ∀ (i : n), ⋯.eigenvalues i ≠ 0

theorem HermitianMat.nonSingular_iff_det_ne_zero {n : Type u_1} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A : HermitianMat n 𝕜} :

A.NonSingular ↔ (↑A).det ≠ 0

theorem HermitianMat.nonSingular_iff_ker_bot {n : Type u_1} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A : HermitianMat n 𝕜} :

A.NonSingular ↔ A.ker = ⊥

theorem HermitianMat.nonSingular_iff_support_top {n : Type u_1} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A : HermitianMat n 𝕜} :

A.NonSingular ↔ A.support = ⊤

@[simp]

theorem HermitianMat.nonSingular_iff_neg {n : Type u_1} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A : HermitianMat n 𝕜} :

(-A).NonSingular ↔ A.NonSingular

@[simp]

theorem HermitianMat.nonSingular_iff_inv {n : Type u_1} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A : HermitianMat n 𝕜} :

A⁻¹.NonSingular ↔ A.NonSingular

@[simp]

theorem HermitianMat.nonSingular_iff_kronecker {n : Type u_1} {m : Type u_2} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] [RCLike 𝕜] {A : HermitianMat n 𝕜} {B : HermitianMat m 𝕜} [Nonempty n] [Nonempty m] :

(A.kronecker B).NonSingular ↔ A.NonSingular ∧ B.NonSingular

theorem HermitianMat.nonSingular_iff_conj {n : Type u_1} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A : HermitianMat n 𝕜} {C : Matrix n n 𝕜} (hC : IsUnit C) :

((conj C) A).NonSingular ↔ A.NonSingular

@[simp]

theorem HermitianMat.nonSingular_iff_reindex {n : Type u_1} {m : Type u_2} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] [RCLike 𝕜] {A : HermitianMat n 𝕜} (e : n ≃ m) :

(A.reindex e).NonSingular ↔ A.NonSingular

theorem HermitianMat.nonSingular_empty {n : Type u_1} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A : HermitianMat n 𝕜} [IsEmpty n] :

theorem HermitianMat.nonSingular_det_ne_zero {n : Type u_1} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A : HermitianMat n 𝕜} [A.NonSingular] :

(↑A).det ≠ 0

@[simp]

theorem HermitianMat.nonSingular_ker_bot {n : Type u_1} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A : HermitianMat n 𝕜} [A.NonSingular] :

@[simp]

theorem HermitianMat.nonSingular_support_top {n : Type u_1} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A : HermitianMat n 𝕜} [A.NonSingular] :

A.support = ⊤

instance HermitianMat.nonSingular_neg {n : Type u_1} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A : HermitianMat n 𝕜} [A.NonSingular] :

(-A).NonSingular

instance HermitianMat.nonSingular_inv {n : Type u_1} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A : HermitianMat n 𝕜} [A.NonSingular] :

A⁻¹.NonSingular

instance HermitianMat.nonSingular_kron {n : Type u_1} {m : Type u_2} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] [RCLike 𝕜] {A : HermitianMat n 𝕜} {B : HermitianMat m 𝕜} [A.NonSingular] [B.NonSingular] [Nonempty n] [Nonempty m] :

(A.kronecker B).NonSingular

theorem HermitianMat.nonSingular_conj {n : Type u_1} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A : HermitianMat n 𝕜} {C : Matrix n n 𝕜} [A.NonSingular] (hC : IsUnit C) :

((conj C) A).NonSingular

instance HermitianMat.nonSingular_conj_isometry {n : Type u_1} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A : HermitianMat n 𝕜} [A.NonSingular] {B : HermitianMat n 𝕜} [B.NonSingular] :

((conj ↑B) A).NonSingular

theorem HermitianMat.nonSingular_zero_notMem_spectrum {n : Type u_1} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A : HermitianMat n 𝕜} [A.NonSingular] :

0 ∉ spectrum ℝ ↑A

theorem HermitianMat.nonSingular_eigenvalue_ne_zero {n : Type u_1} {𝕜 : Type u_4} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A : HermitianMat n 𝕜} [A.NonSingular] (i : n) :

⋯.eigenvalues i ≠ 0