Gershgorin

📁 Source: Mathlib/LinearAlgebra/Matrix/Gershgorin.lean

Statistics

Metric	Count
Definitions	0
Theorems det_ne_zero_of_sum_col_lt_diag, det_ne_zero_of_sum_row_lt_diag, eigenvalue_mem_ball	3
Total	3

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det_ne_zero_of_sum_col_lt_diag 📖	—	Real Real.instLT Finset.sum Real.instAddCommMonoid Finset.erase Finset.univ Norm.norm NormedField.toNorm	—	—	Matrix.det_transpose det_ne_zero_of_sum_row_lt_diag Finset.sum_congr
det_ne_zero_of_sum_row_lt_diag 📖	—	Real Real.instLT Finset.sum Real.instAddCommMonoid Finset.erase Finset.univ Norm.norm NormedField.toNorm	—	—	Mathlib.Tactic.Contrapose.contrapose₃ Mathlib.Tactic.Push.not_forall_eq eigenvalue_mem_ball RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass Module.End.hasEigenvalue_iff Module.End.eigenspace_zero ne_of_lt LinearMap.bot_lt_ker_of_det_eq_zero instIsDomain Module.Free.function Finite.of_fintype Module.Free.self LinearMap.det_toLin' sub_zero mem_closedBall_iff_norm'
eigenvalue_mem_ball 📖	mathematical	Module.End.HasEigenvalue EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField Pi.addCommGroup NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing Pi.Function.module CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Matrix LinearMap Pi.addCommMonoid Matrix.addCommMonoid LinearMap.addCommMonoid Matrix.module LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLin'	Set Set.instMembership Metric.closedBall SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Finset.sum Real Real.instAddCommMonoid Finset.erase Finset.univ Norm.norm NormedField.toNorm	—	RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass isEmpty_or_nonempty Submodule.eq_bot_of_subsingleton instSubsingletonSubtype_mathlib Unique.instSubsingleton Module.End.HasEigenvalue.exists_hasEigenvector Finset.univ_nonempty Finset.exists_mem_eq_sup' Mathlib.Tactic.Contrapose.contrapose₄ Pi.zero_apply norm_le_zero_iff LE.le.trans Finset.le_sup' Finset.mem_univ norm_mul NormedDivisionRing.toNormMulClass norm_inv mul_inv_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing norm_pos_iff one_mul Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add dotProduct.eq_1 Matrix.mulVec.eq_1 Module.End.mem_eigenspace_iff Finset.sum_erase_eq_sub neg_sub neg_mul norm_neg Finset.sum_mul norm_sum_le le_of_eq Finset.sum_congr mul_assoc Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_le_of_le_one_right IsOrderedRing.toPosMulMono Real.instIsOrderedRing norm_nonneg

---

← Back to Index