Symmetric

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

Statistics

Metric	Count
Definitions IsSymm, instDecidableIsSymmOfEqTranspose	2
Theorems add, apply, conjTranspose, eq, ext, ext_iff, fromBlocks, map, neg, pow, reindex, smul, sub, submatrix, transpose, isSymm_add_transpose_self, isSymm_comp_iff, isSymm_comp_iff_forall, isSymm_conjTranspose_iff, isSymm_diagonal, isSymm_fromBlocks_iff, isSymm_map_iff, isSymm_mul_transpose_self, isSymm_neg_iff, isSymm_one, isSymm_reindex_iff, isSymm_smul_iff, isSymm_transpose_add_self, isSymm_transpose_iff, isSymm_transpose_mul_self, isSymm_zero	31
Total	33

Matrix

Definitions

Name	Category	Theorems
IsSymm 📖	MathDef	51 math math: isSymm_reindex_iff, IsSymm.exp, IsSymm.map, IsSymm.pow, CartanMatrix.D_isSymm, isSymm_smul_iff, IsSymm.reindex, IsSymm.smul, SimpleGraph.isSymm_adjMatrix, isSymm_zero, IsSymm.conjTranspose, isSymm_add_transpose_self, IsSymm.zpow, CartanMatrix.E₇_isSymm, isSymm_mul_transpose_self, CartanMatrix.A_isSymm, isSymm_map_iff, IsSymm.transpose, CoxeterMatrix.isSymm, SimpleGraph.isSymm_lapMatrix, QuadraticMap.isSymm_toMatrix', isSymm_comp_iff_forall, CartanMatrix.E₈_isSymm, SimpleGraph.isSymm_degMatrix, isAdjMatrix_iff_hadamard, IsAdjMatrix.symm, isSymm_conjTranspose_iff, IsSymm.submatrix, isSymm_comp_iff, isSymm_iff_intrinsicStar_toLin', isSymm_neg_iff, Fin.circulant_isSymm_iff, isSymm_transpose_add_self, isSymm_fromBlocks_iff, isSymm_swap, IsSymm.neg, IsSymm.adjugate, IsSymm.ext_iff, isSymm_compl, circulant_isSymm_iff, IsSymm.inv, IsSymm.fromBlocks, isSymm_one, IsSymm.sub, IsDiag.isSymm, isSymm_transpose_mul_self, isSymm_diagonal, IsSymm.add, isSymm_transpose_iff, CartanMatrix.E₆_isSymm, IsSymm.ext
instDecidableIsSymmOfEqTranspose 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSymm_add_transpose_self 📖	mathematical	—	IsSymm Matrix add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma transpose	—	add_comm
isSymm_comp_iff 📖	mathematical	—	IsSymm DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike comp transpose map	—	IsSymm.eq_1 transpose_comp transpose_map Equiv.injective Function.Involutive.eq_iff transpose_involutive
isSymm_comp_iff_forall 📖	mathematical	—	IsSymm DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike comp	—	—
isSymm_conjTranspose_iff 📖	mathematical	—	IsSymm conjTranspose InvolutiveStar.toStar	—	conjTranspose_conjTranspose IsSymm.conjTranspose
isSymm_diagonal 📖	mathematical	—	IsSymm diagonal	—	diagonal_transpose
isSymm_fromBlocks_iff 📖	mathematical	—	IsSymm fromBlocks transpose	—	IsSymm.fromBlocks
isSymm_map_iff 📖	mathematical	—	IsSymm map	—	IsSymm.eq_1 transpose_map map_injective
isSymm_mul_transpose_self 📖	mathematical	—	IsSymm Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalNonAssocSemiring.toAddCommMonoid transpose	—	transpose_mul
isSymm_neg_iff 📖	mathematical	—	IsSymm Matrix neg InvolutiveNeg.toNeg	—	neg_neg IsSymm.neg
isSymm_one 📖	mathematical	—	IsSymm Matrix one	—	transpose_one
isSymm_reindex_iff 📖	mathematical	—	IsSymm DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike reindex	—	submatrix_submatrix Equiv.symm_comp_self submatrix_id_id IsSymm.reindex
isSymm_smul_iff 📖	mathematical	—	IsSymm Matrix smul SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	invOf_smul_smul IsSymm.smul
isSymm_transpose_add_self 📖	mathematical	—	IsSymm Matrix add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma transpose	—	add_comm
isSymm_transpose_iff 📖	mathematical	—	IsSymm transpose	—	transpose_transpose IsSymm.transpose
isSymm_transpose_mul_self 📖	mathematical	—	IsSymm Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalNonAssocSemiring.toAddCommMonoid transpose	—	transpose_mul
isSymm_zero 📖	mathematical	—	IsSymm Matrix zero	—	transpose_zero

Matrix.IsSymm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	Matrix.IsSymm	Matrix.IsSymm Matrix Matrix.add	—	Matrix.transpose_add
apply 📖	—	Matrix.IsSymm	—	—	ext_iff
conjTranspose 📖	mathematical	Matrix.IsSymm	Matrix.IsSymm Matrix.conjTranspose	—	map transpose
eq 📖	mathematical	Matrix.IsSymm	Matrix.transpose	—	—
ext 📖	mathematical	—	Matrix.IsSymm	—	Matrix.ext
ext_iff 📖	mathematical	—	Matrix.IsSymm	—	Matrix.ext_iff
fromBlocks 📖	mathematical	Matrix.IsSymm Matrix.transpose	Matrix.IsSymm Matrix.fromBlocks	—	Matrix.transpose_transpose Matrix.fromBlocks_transpose
map 📖	mathematical	Matrix.IsSymm	Matrix.IsSymm Matrix.map	—	eq_1 Matrix.transpose_map eq
neg 📖	mathematical	Matrix.IsSymm	Matrix.IsSymm Matrix Matrix.neg	—	Matrix.transpose_neg
pow 📖	mathematical	Matrix.IsSymm	Matrix.IsSymm Matrix Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring	—	eq_1 Matrix.transpose_pow
reindex 📖	mathematical	Matrix.IsSymm	Matrix.IsSymm DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike Matrix.reindex	—	Matrix.reindex_apply submatrix
smul 📖	mathematical	Matrix.IsSymm	Matrix.IsSymm Matrix Matrix.smul	—	Matrix.transpose_smul
sub 📖	mathematical	Matrix.IsSymm	Matrix.IsSymm Matrix Matrix.sub	—	Matrix.transpose_sub
submatrix 📖	mathematical	Matrix.IsSymm	Matrix.IsSymm Matrix.submatrix	—	Matrix.transpose_submatrix
transpose 📖	mathematical	Matrix.IsSymm	Matrix.IsSymm Matrix.transpose	—	—

---

← Back to Index