matrix

📁 Source: MathlibTest/matrix.lean

Statistics

Metric	Count
Definitions matrix, matrix, matrix, matrix, matrix, matrix, matrix, matrix, matrix, matrix, matrix, matrix	12
Theorems matrix, matrix, matrix, matrix, matrix, matrix, matrix, matrix, matrix, matrix	10
Total	22

AddSubgroup

Definitions

Name	Category	Theorems
matrix 📖	CompOp	1 math math: coe_matrix

AddSubmonoid

Definitions

Name	Category	Theorems
matrix 📖	CompOp	4 math math: Subring.coe_matrix, Subalgebra.coe_matrix, Subsemiring.coe_matrix, coe_matrix

Algebra.IsCentral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
matrix 📖	mathematical	—	Algebra.IsCentral Matrix Matrix.semiring Matrix.instAlgebra	—	Eq.trans_le Matrix.subalgebraCenter_eq_scalarAlgHom_map LE.le.trans_eq Subalgebra.map_mono out Algebra.map_bot

CategoryTheory.Limits.biproduct

Definitions

Name	Category	Theorems
matrix 📖	CompOp	22 math math: CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality, matrixEquiv_symm_apply, CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality', matrix_desc_assoc, lift_matrix_assoc, ι_matrix, ι_matrix_assoc, matrix_map_assoc, components_matrix, matrix_map, matrix_π, matrix_desc, matrix_π_assoc, CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv_symm_apply, CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality_assoc, map_matrix_assoc, map_matrix, lift_matrix, CategoryTheory.Mat_.lift_map, matrix_components, CategoryTheory.HomOrthogonal.matrixDecomposition_symm_apply, CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality'_assoc

Ideal

Definitions

Name	Category	Theorems
matrix 📖	CompOp	8 math math: single_mem_jacobson_matrix, mem_matrix, matrix_top, matrix_jacobson_le, matrix_strictMono_of_nonempty, TwoSidedIdeal.asIdeal_matrix, matrix_bot, matrix_monotone

IsAzumaya

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
matrix 📖	mathematical	—	IsAzumaya Matrix Matrix.semiring CommSemiring.toSemiring Matrix.instAlgebra Algebra.id	—	Module.Projective.of_free Module.Free.matrix Module.Free.self Finite.of_fintype Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Matrix.subsingleton FaithfulSMul.eq_of_smul_eq_smul Module.Free.instFaithfulSMulOfNontrivial Matrix.nonempty Module.Finite.matrix Module.Finite.self smulCommClass_self IsScalarTower.left Function.bijective_iff_has_inverse Matrix.smulCommClass Algebra.to_smulCommClass DFunLike.congr_fun RingHomCompTriple.ids AlgHom.mulLeftRightMatrix.inv_comp AlgHom.mulLeftRightMatrix.comp_inv

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
matrix 📖	mathematical	IsCompact	Matrix instTopologicalSpaceMatrix Set.matrix	—	isCompact_pi_infinite

IsLeftRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
matrix 📖	mathematical	IsLeftRegular	IsSMulRegular Matrix Matrix.smul	—	IsSMulRegular.matrix isSMulRegular

IsMoritaEquivalent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
matrix 📖	mathematical	—	IsMoritaEquivalent CommRing.toCommSemiring Matrix Matrix.instRing Matrix.instAlgebra Ring.toSemiring	—	Nonempty.map

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
matrix 📖	mathematical	IsOpen	Matrix instTopologicalSpaceMatrix Set.matrix	—	preimage continuous_id isOpen_set_pi Set.finite_univ Set.matrix_eq_pi

IsSMulRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
matrix 📖	mathematical	IsSMulRegular	Matrix Matrix.smul	—	pi

IsSimpleRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
matrix 📖	mathematical	—	IsSimpleRing Matrix Matrix.nonUnitalNonAssocRing NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	OrderIso.isSimpleOrder simple

Module.Basis

Definitions

Name	Category	Theorems
matrix 📖	CompOp	1 math math: matrix_apply

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
matrix 📖	mathematical	—	Module.Finite Matrix Matrix.addCommMonoid Matrix.module	—	nonempty_fintype of_basis Finite.instProd Finite.of_fintype

Module.Free

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
matrix 📖	mathematical	—	Module.Free Matrix Matrix.addCommMonoid Matrix.module	—	pi function

RingCon

Definitions

Name	Category	Theorems
matrix 📖	CompOp	10 math math: matrix_strictMono_of_nonempty, matrix_top, ofMatrix_matrix, matrix_ofMatrix, matrix_injective, matrix_bot, matrix_apply_single, TwoSidedIdeal.matrix_ringCon, matrix_apply, matrix_monotone

Set

Definitions

Name	Category	Theorems
matrix 📖	CompOp	11 math math: Matrix.diagonal_mem_matrix_iff, mem_matrix, Matrix.single_mem_matrix, AddSubgroup.coe_matrix, Matrix.transpose_mem_matrix_iff, IsCompact.matrix, AddSubmonoid.coe_matrix, Submodule.coe_matrix, matrix_eq_pi, IsOpen.matrix, Matrix.submatrix_mem_matrix_iff

Subalgebra

Definitions

Name	Category	Theorems
matrix 📖	CompOp	1 math math: coe_matrix

Submodule

Definitions

Name	Category	Theorems
matrix 📖	CompOp	1 math math: coe_matrix

Subring

Definitions

Name	Category	Theorems
matrix 📖	CompOp	1 math math: coe_matrix

Subsemiring

Definitions

Name	Category	Theorems
matrix 📖	CompOp	1 math math: coe_matrix

TwoSidedIdeal

Definitions

Name	Category	Theorems
matrix 📖	CompOp	10 math math: matrix_jacobson_bot, equivMatrix_apply, matrix_top, matrix_bot, jacobson_matrix, mem_matrix, matrix_monotone, asIdeal_matrix, matrix_ringCon, matrix_strictMono_of_nonempty

---

← Back to Index