Ideal

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

Statistics

Metric	Count
Definitions ofMatrix, equivMatrix, orderIsoMatrix	3
Theorems matrix_bot, matrix_jacobson_le, matrix_monotone, matrix_strictMono_of_nonempty, matrix_top, mem_matrix, single_mem_jacobson_matrix, coe_ofMatrix_eq_relationMap, matrix_apply, matrix_apply_single, matrix_bot, matrix_injective, matrix_monotone, matrix_ofMatrix, matrix_strictMono_of_nonempty, matrix_top, ofMatrix_matrix, ofMatrix_rel, ofMatrix_rel', asIdeal_matrix, coe_equivMatrix_symm_apply, equivMatrix_apply, equivMatrix_symm_apply_ringCon, jacobson_matrix, matrix_bot, matrix_jacobson_bot, matrix_monotone, matrix_ringCon, matrix_strictMono_of_nonempty, matrix_top, mem_matrix, orderIsoMatrix_apply_ringCon_r, orderIsoMatrix_symm_apply_ringCon_r	33
Total	36

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
matrix_bot 📖	mathematical	—	matrix Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Matrix Matrix.semiring	—	ext Matrix.ext
matrix_jacobson_le 📖	mathematical	—	Ideal Matrix Matrix.semiring Ring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule matrix jacobson Matrix.instRing	—	Matrix.matrix_eq_sum_single sum_mem Submodule.addSubmonoidClass single_mem_jacobson_matrix
matrix_monotone 📖	mathematical	—	Monotone Ideal Matrix Matrix.semiring PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule matrix	—	—
matrix_strictMono_of_nonempty 📖	mathematical	—	StrictMono Ideal Matrix Matrix.semiring PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule matrix	—	Monotone.strictMono_of_injective matrix_monotone ext
matrix_top 📖	mathematical	—	matrix Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Matrix Matrix.semiring	—	ext
mem_matrix 📖	mathematical	—	Matrix Ideal Matrix.semiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule matrix	—	—
single_mem_jacobson_matrix 📖	mathematical	Ideal Ring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule jacobson	Matrix Matrix.instRing matrix Matrix.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	eq_or_ne Finset.sum_congr ite_and sub_mul one_mul mul_ite MulZeroClass.mul_zero Finset.sum_ite_eq Matrix.sum_apply Finset.sum_ite_eq' ite_mul MulZeroClass.zero_mul sub_sub_cancel Matrix.one_apply_eq Matrix.one_apply_ne zero_sub sub_zero neg_mul mul_assoc sub_add sub_neg_eq_add mul_sub mul_add Distrib.leftDistribClass mul_one neg_sub mul_mem_left Matrix.single_apply_of_ne Finset.sum_const_zero zero_add sub_self AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass

RingCon

Definitions

Name	Category	Theorems
ofMatrix 📖	CompOp	6 math math: TwoSidedIdeal.equivMatrix_symm_apply_ringCon, ofMatrix_rel, coe_ofMatrix_eq_relationMap, ofMatrix_matrix, ofMatrix_rel', matrix_ofMatrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_ofMatrix_eq_relationMap 📖	mathematical	—	DFunLike.coe RingCon Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toMul instFunLikeForallProp ofMatrix Relation.Map Matrix Matrix.add Matrix.instMulOfFintypeOfAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid	—	Matrix.single_apply_same Matrix.single_mul_mul_single one_mul mul_one mul refl
matrix_apply 📖	mathematical	—	DFunLike.coe RingCon Matrix Matrix.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Matrix.instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toAddCommMonoid instFunLikeForallProp matrix	—	—
matrix_apply_single 📖	mathematical	—	DFunLike.coe RingCon Matrix Matrix.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Matrix.instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toAddCommMonoid instFunLikeForallProp matrix Matrix.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Matrix.single_apply_same ne_or_eq Matrix.single_apply_of_ne refl
matrix_bot 📖	mathematical	—	matrix Bot.bot RingCon Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Distrib.toMul OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Matrix Matrix.add Matrix.instMulOfFintypeOfAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid	—	eq_bot_iff Matrix.ext
matrix_injective 📖	mathematical	—	RingCon Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Distrib.toMul Matrix Matrix.add Matrix.instMulOfFintypeOfAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid matrix	—	ext DFunLike.congr_fun
matrix_monotone 📖	mathematical	—	Monotone RingCon Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Distrib.toMul Matrix Matrix.add Matrix.instMulOfFintypeOfAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid PartialOrder.toPreorder instPartialOrder matrix	—	—
matrix_ofMatrix 📖	mathematical	—	matrix NonAssocSemiring.toNonUnitalNonAssocSemiring ofMatrix	—	ext Matrix.matrix_eq_sum_single AddCon.finset_sum Matrix.single_mul_mul_single one_mul mul_one mul refl
matrix_strictMono_of_nonempty 📖	mathematical	—	StrictMono RingCon Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Distrib.toMul Matrix Matrix.add Matrix.instMulOfFintypeOfAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid PartialOrder.toPreorder instPartialOrder matrix	—	Monotone.strictMono_of_injective matrix_monotone matrix_injective
matrix_top 📖	mathematical	—	matrix Top.top RingCon Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Distrib.toMul OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Matrix Matrix.add Matrix.instMulOfFintypeOfAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid	—	eq_top_iff
ofMatrix_matrix 📖	mathematical	—	ofMatrix matrix	—	ext Matrix.single_apply_same matrix_apply_single
ofMatrix_rel 📖	mathematical	—	DFunLike.coe RingCon Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Distrib.toMul instFunLikeForallProp ofMatrix Matrix Matrix.add Matrix.instMulOfFintypeOfAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
ofMatrix_rel' 📖	mathematical	—	DFunLike.coe RingCon Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toMul instFunLikeForallProp ofMatrix Matrix Matrix.add Matrix.instMulOfFintypeOfAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Matrix.single_mul_single_same one_mul mul_one mul refl

TwoSidedIdeal

Definitions

Name	Category	Theorems
equivMatrix 📖	CompOp	3 math math: equivMatrix_symm_apply_ringCon, equivMatrix_apply, coe_equivMatrix_symm_apply
orderIsoMatrix 📖	CompOp	2 math math: orderIsoMatrix_apply_ringCon_r, orderIsoMatrix_symm_apply_ringCon_r

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
asIdeal_matrix 📖	mathematical	—	DFunLike.coe OrderHom TwoSidedIdeal Matrix NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Matrix.instRing Ideal Ring.toSemiring PartialOrder.toPreorder instPartialOrder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule OrderHom.instFunLike asIdeal matrix Ideal.matrix	—	Ideal.ext
coe_equivMatrix_symm_apply 📖	mathematical	—	SetLike.coe TwoSidedIdeal NonAssocRing.toNonUnitalNonAssocRing setLike DFunLike.coe Equiv Matrix Matrix.nonUnitalNonAssocRing EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivMatrix setOf SetLike.instMembership	—	Set.ext Matrix.single_zero Matrix.single_apply_same SetLike.mem_coe mem_iff equivMatrix_symm_apply_ringCon RingCon.coe_ofMatrix_eq_relationMap
equivMatrix_apply 📖	mathematical	—	DFunLike.coe Equiv TwoSidedIdeal NonAssocRing.toNonUnitalNonAssocRing Matrix Matrix.nonUnitalNonAssocRing EquivLike.toFunLike Equiv.instEquivLike equivMatrix matrix	—	—
equivMatrix_symm_apply_ringCon 📖	mathematical	—	ringCon NonAssocRing.toNonUnitalNonAssocRing DFunLike.coe Equiv TwoSidedIdeal Matrix Matrix.nonUnitalNonAssocRing EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivMatrix RingCon.ofMatrix NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	—	—
jacobson_matrix 📖	mathematical	—	jacobson Matrix Matrix.instRing matrix NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	le_antisymm asIdeal_jacobson asIdeal_matrix
matrix_bot 📖	mathematical	—	matrix Bot.bot TwoSidedIdeal instBot Matrix Matrix.nonUnitalNonAssocRing	—	ringCon_injective RingCon.matrix_bot
matrix_jacobson_bot 📖	mathematical	—	matrix NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing jacobson Bot.bot TwoSidedIdeal instBot Matrix Matrix.instRing Matrix.nonUnitalNonAssocRing	—	jacobson_matrix matrix_bot
matrix_monotone 📖	mathematical	—	Monotone TwoSidedIdeal Matrix Matrix.nonUnitalNonAssocRing PartialOrder.toPreorder instPartialOrder matrix	—	—
matrix_ringCon 📖	mathematical	—	ringCon Matrix Matrix.nonUnitalNonAssocRing matrix RingCon.matrix NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	—	—
matrix_strictMono_of_nonempty 📖	mathematical	—	StrictMono TwoSidedIdeal Matrix Matrix.nonUnitalNonAssocRing PartialOrder.toPreorder instPartialOrder matrix	—	Monotone.strictMono_of_injective matrix_monotone RingCon.matrix_injective ringCon_injective
matrix_top 📖	mathematical	—	matrix Top.top TwoSidedIdeal instTop Matrix Matrix.nonUnitalNonAssocRing	—	ringCon_injective RingCon.matrix_top
mem_matrix 📖	mathematical	—	Matrix TwoSidedIdeal Matrix.nonUnitalNonAssocRing SetLike.instMembership setLike matrix	—	—
orderIsoMatrix_apply_ringCon_r 📖	mathematical	—	Matrix Con.toSetoid Matrix.instMulOfFintypeOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing NonUnitalNonAssocSemiring.toAddCommMonoid RingCon.toCon Matrix.add Distrib.toAdd ringCon Matrix.nonUnitalNonAssocRing DFunLike.coe RelIso TwoSidedIdeal Preorder.toLE PartialOrder.toPreorder instPartialOrder RelIso.instFunLike orderIsoMatrix	—	—
orderIsoMatrix_symm_apply_ringCon_r 📖	mathematical	—	Con.toSetoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing RingCon.toCon Distrib.toAdd ringCon DFunLike.coe RelIso TwoSidedIdeal Matrix Matrix.nonUnitalNonAssocRing Preorder.toLE PartialOrder.toPreorder instPartialOrder RelIso.instFunLike RelIso.symm orderIsoMatrix	—	—

---

← Back to Index