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, smul, sub, submatrix, transpose, isSymm_add_transpose_self, isSymm_diagonal, isSymm_fromBlocks_iff, isSymm_mul_transpose_self, isSymm_one, isSymm_transpose_add_self, isSymm_transpose_mul_self, isSymm_zero	22
Total	24

Matrix

Definitions

Name	Category	Theorems
IsSymm 📖	MathDef	25 math math: CartanMatrix.D_isSymm, SimpleGraph.isSymm_adjMatrix, isSymm_zero, isSymm_add_transpose_self, CartanMatrix.E₇_isSymm, isSymm_mul_transpose_self, CartanMatrix.A_isSymm, CoxeterMatrix.isSymm, SimpleGraph.isSymm_lapMatrix, QuadraticMap.isSymm_toMatrix', CartanMatrix.E₈_isSymm, SimpleGraph.isSymm_degMatrix, isAdjMatrix_iff_hadamard, IsAdjMatrix.symm, Fin.circulant_isSymm_iff, isSymm_transpose_add_self, isSymm_fromBlocks_iff, IsSymm.ext_iff, circulant_isSymm_iff, isSymm_one, IsDiag.isSymm, isSymm_transpose_mul_self, isSymm_diagonal, 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_diagonal 📖	mathematical	—	IsSymm diagonal	—	diagonal_transpose
isSymm_fromBlocks_iff 📖	mathematical	—	IsSymm fromBlocks transpose	—	IsSymm.fromBlocks
isSymm_mul_transpose_self 📖	mathematical	—	IsSymm Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalNonAssocSemiring.toAddCommMonoid transpose	—	transpose_mul
isSymm_one 📖	mathematical	—	IsSymm Matrix one	—	transpose_one
isSymm_transpose_add_self 📖	mathematical	—	IsSymm Matrix add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma transpose	—	add_comm
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 Matrix.add	—	Matrix.transpose_add
apply 📖	—	Matrix.IsSymm	—	—	ext_iff
conjTranspose 📖	mathematical	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.fromBlocks	—	Matrix.transpose_transpose Matrix.fromBlocks_transpose
map 📖	mathematical	Matrix.IsSymm	Matrix.map	—	Matrix.transpose_map
neg 📖	mathematical	Matrix.IsSymm	Matrix Matrix.neg	—	Matrix.transpose_neg
pow 📖	mathematical	Matrix.IsSymm	Matrix Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring CommSemiring.toSemiring	—	eq_1 Matrix.transpose_pow
smul 📖	mathematical	Matrix.IsSymm	Matrix Matrix.smul	—	Matrix.transpose_smul
sub 📖	mathematical	Matrix.IsSymm	Matrix Matrix.sub	—	Matrix.transpose_sub
submatrix 📖	mathematical	Matrix.IsSymm	Matrix.submatrix	—	Matrix.transpose_submatrix
transpose 📖	mathematical	Matrix.IsSymm	Matrix.transpose	—	—

---

← Back to Index