WithConv

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

Statistics

Metric	Count
Definitions `WithConv`, `matrixToLin'StarAlgEquiv`, `instAlgebraWithConvMatrix`, `instCommMagmaWithConvMatrix`, `instCommMonoidWithConvMatrix`, `instCommRingWithConvMatrix`, `instCommSemiringWithConvMatrix`, `instInvolutiveStarWithConvMatrix`, `instMonoidWithConvMatrix`, `instMulOneClassWithConvMatrix`, `instMulWithConvMatrix`, `instNonAssocCommRingWithConvMatrix`, `instNonAssocCommSemiringWithConvMatrix`, `instNonAssocRingWithConvMatrix`, `instNonAssocSemiringWithConvMatrix`, `instNonUnitalCommRingWithConvMatrix`, `instNonUnitalCommSemiringWithConvMatrix`, `instNonUnitalNonAssocCommRingWithConvMatrix`, `instNonUnitalNonAssocCommSemiringWithConvMatrix`, `instNonUnitalNonAssocRingWithConvMatrix`, `instNonUnitalNonAssocSemiringWithConvMatrix`, `instNonUnitalRingWithConvMatrix`, `instNonUnitalSemiringWithConvMatrix`, `instOneWithConvMatrix`, `instRingWithConvMatrix`, `instSemigroupWithConvMatrix`, `instSemiringWithConvMatrix`, `instStarAddMonoidWithConvMatrix`, `instStarMulWithConvMatrix`, `instStarRingWithConvMatrix`, `instStarWithConvMatrix`	31
Theorems `isSelfAdjoint`, `isSymm_iff_intrinsicStar_toLin'`, `toLin'_hadamard`, `matrixToLin'StarAlgEquiv_apply`, `symm_matrixToLin'StarAlgEquiv_apply`, `convMul_def`, `convOne_def`, `instIsScalarTowerWithConvMatrix`, `instSMulCommClassWithConvMatrix`, `intrinsicStar_def`	10
Total	41

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSymm_iff_intrinsicStar_toLin'` 📖	mathematical	—	`IsSymm` `Star.star` `WithConv` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `LinearMap.intrinsicStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `StarRing.toStarAddMonoid` `Pi.instStarAddMonoidForall` `Pi.instStarModuleForall` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `InvolutiveStar.toStar` `StarMul.toStarModule` `CommSemiring.toCommMonoid` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `WithConv.toConv` `DFunLike.coe` `LinearEquiv` `RingHomInvPair.ids` `Matrix` `addCommMonoid` `LinearMap.addCommMonoid` `module` `LinearMap.module` `Function.smulCommClass` `DistribMulAction.toMulAction` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toLin'` `instStar`	—	`Pi.instStarModuleForall` `StarMul.toStarModule` `RingHomInvPair.ids` `Function.smulCommClass` `Algebra.to_smulCommClass` `intrinsicStar_toLin'` `WithConv.toConv_injective` `LinearEquiv.injective` `transpose_conjTranspose` `star_eq_conjTranspose` `IsSymm.eq_1`
`toLin'_hadamard` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Matrix` `LinearMap` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `addCommMonoid` `LinearMap.addCommMonoid` `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` `toLin'` `hadamard` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `WithConv.ofConv` `WithConv` `LinearMap.convMul` `Pi.nonUnitalNonAssocSemiring` `Pi.semiring` `Function.algebra` `IsScalarTower.right` `Pi.instCoalgebraStruct` `Coalgebra.toCoalgebraStruct` `CommSemiring.toCoalgebra` `WithConv.toConv`	—	`LinearMap.pi_ext'` `Finite.of_fintype` `RingHomInvPair.ids` `Function.smulCommClass` `Algebra.to_smulCommClass` `IsScalarTower.right` `LinearMap.ext_ring` `RingHomCompTriple.ids` `mulVec_single` `one_smul` `Pi.comul_single`

Matrix.WithConv.IsIdempotentElem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSelfAdjoint` 📖	mathematical	`IsIdempotentElem` `WithConv` `Matrix` `instMulWithConvMatrix` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`IsSelfAdjoint` `WithConv` `Matrix` `instStarWithConvMatrix` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid`	—	`IsSelfAdjoint.eq_1` `WithConv.ext_iff` `Matrix.ext` `star_zero` `star_one`

WithConv

Definitions

Name	Category	Theorems
`matrixToLin'StarAlgEquiv` 📖	CompOp	2 math math: `matrixToLin'StarAlgEquiv_apply`, `symm_matrixToLin'StarAlgEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`matrixToLin'StarAlgEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgEquiv` `WithConv` `Matrix` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `instNonUnitalNonAssocSemiringWithConvMatrix` `LinearMap.convNonUnitalNonAssocSemiring` `Pi.nonUnitalNonAssocSemiring` `Algebra.to_smulCommClass` `Pi.semiring` `Function.algebra` `Algebra.id` `IsScalarTower.right` `Pi.instCoalgebraStruct` `Coalgebra.toCoalgebraStruct` `CommSemiring.toCoalgebra` `instMulWithConvMatrix` `Distrib.toMul` `LinearMap.convMul` `Algebra.toSMul` `instSemiringWithConvMatrix` `instAlgebraWithConvMatrix` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddMonoid` `AddCommMonoid.toAddMonoid` `LinearMap.addCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instDistribMulAction` `LinearMap.instDistribMulAction` `Pi.distribMulAction` `Module.toDistribMulAction` `Function.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `instStarWithConvMatrix` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `StarRing.toStarAddMonoid` `LinearMap.intrinsicStar` `Pi.instStarAddMonoidForall` `Pi.instStarModuleForall` `StarMul.toStarModule` `CommSemiring.toCommMonoid` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `StarAlgEquiv.instFunLike` `matrixToLin'StarAlgEquiv` `toConv` `LinearEquiv` `RingHomInvPair.ids` `Matrix.addCommMonoid` `Matrix.module` `LinearMap.module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Matrix.toLin'` `ofConv`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `Function.smulCommClass` `Pi.instStarModuleForall` `StarMul.toStarModule`
`symm_matrixToLin'StarAlgEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgEquiv` `WithConv` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `Matrix` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `LinearMap.convNonUnitalNonAssocSemiring` `Pi.nonUnitalNonAssocSemiring` `Algebra.to_smulCommClass` `Pi.semiring` `Function.algebra` `Algebra.id` `IsScalarTower.right` `Pi.instCoalgebraStruct` `Coalgebra.toCoalgebraStruct` `CommSemiring.toCoalgebra` `instNonUnitalNonAssocSemiringWithConvMatrix` `LinearMap.convMul` `instMulWithConvMatrix` `Distrib.toMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddMonoid` `AddCommMonoid.toAddMonoid` `LinearMap.addCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instDistribMulAction` `LinearMap.instDistribMulAction` `Pi.distribMulAction` `Module.toDistribMulAction` `Function.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `Algebra.toSMul` `instSemiringWithConvMatrix` `instAlgebraWithConvMatrix` `LinearMap.intrinsicStar` `StarAddMonoid.toInvolutiveStar` `StarRing.toStarAddMonoid` `Pi.instStarAddMonoidForall` `Pi.instStarModuleForall` `InvolutiveStar.toStar` `StarMul.toStarModule` `CommSemiring.toCommMonoid` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `instStarWithConvMatrix` `StarAlgEquiv.instFunLike` `StarAlgEquiv.symm` `matrixToLin'StarAlgEquiv` `toConv` `LinearEquiv` `RingHomInvPair.ids` `Matrix.addCommMonoid` `LinearMap.module` `Matrix.module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearMap.toMatrix'` `ofConv`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `Function.smulCommClass` `Pi.instStarModuleForall` `StarMul.toStarModule`

(root)

Definitions

Name	Category	Theorems
`WithConv` 📖	CompData	105 math math: `WithConv.ofConv_eq_zero`, `WithConv.addEquiv_symm_apply_ofConv`, `LinearMap.convMul_def`, `WithConv.toConv_bijective`, `WithConv.toEquiv_addEquiv`, `convOne_def`, `LinearMap.intrinsicStar_mulRight`, `Module.End.spectrum_intrinsicStar`, `ContinuousLinearMap.intrinsicStar_toSpanSingleton`, `WithConv.ofConv_surjective`, `WithConv.ofConv_listSum`, `Matrix.intrinsicStar_toLin'`, `LinearMap.intrinsicStar_toSpanSingleton`, `ContinuousLinearMap.IntrinsicStar.isSelfAdjoint_iff_map_star`, `WithConv.ofConv_injective`, `WithConv.symm_linearEquiv_apply`, `Matrix.toLin'_hadamard`, `Module.End.mem_eigenspace_intrinsicStar_iff`, `ContinuousLinearMap.intrinsicStarModule`, `WithConv.equiv_apply`, `LinearMap.convOne_apply`, `Pi.intrinsicStar_comul_commSemiring`, `WithConv.toConv_sub`, `Matrix.WithConv.IsIdempotentElem.isSelfAdjoint`, `WithConv.toConv_smul`, `LinearMap.intrinsicStar_mul'`, `WithConv.ofConv_zero`, `ContinuousLinearMap.intrinsicStar_comp`, `Pi.intrinsicStar_comul`, `WithConv.toConv_zero`, `LinearMap.IntrinsicStar.starLinearEquiv_eq_arrowCongr`, `LinearMap.intrinsicStar_zero`, `WithConv.congrLinearEquiv_apply`, `WithConv.matrixToLin'StarAlgEquiv_apply`, `ContinuousLinearMap.toLinearMap_intrinsicStar`, `WithConv.symm_congr_apply`, `LinearMap.IntrinsicStar.isSelfAdjoint_iff_map_star`, `LinearMap.intrinsicStar_comp'`, `LinearMap.intrinsicStar_rTensor`, `instIsScalarTowerWithConvMatrix`, `TensorProduct.intrinsicStar_map`, `Matrix.IntrinsicStar.isSelfAdjoint_toLin'_iff`, `ContinuousLinearMap.intrinsicStar_zero`, `ContinuousLinearMap.intrinsicStar_eq_comp`, `LinearMap.toMatrix'_intrinsicStar`, `WithConv.toConv_add`, `WithConv.toEquiv_congrLinearEquiv`, `LinearMap.convOne_def`, `WithConv.toConv_listSum`, `WithConv.linearEquiv_apply`, `WithConv.toConv_neg`, `LinearMap.intrinsicStar_convMul`, `LinearMap.intrinsicStar_id`, `Coalgebra.Repr.convMul_apply`, `WithConv.addEquiv_apply`, `ContinuousLinearMap.intrinsicStar_smulRight`, `LinearMap.intrinsicStar_mulLeft`, `WithConv.symm_congrLinearEquiv`, `LinearMap.nonUnitalAlgHom_comp_convMul_distrib`, `LinearMap.intrinsicStar_lTensor`, `WithConv.symm_congr`, `LinearMap.intrinsicStarModule`, `LinearMap.intrinsicStar_single`, `LinearMap.intrinsicStar_smulRight`, `ContinuousLinearMap.intrinsicStar_comp'`, `WithConv.symm_matrixToLin'StarAlgEquiv_apply`, `ContinuousLinearMap.intrinsicStar_id`, `LinearMap.IntrinsicStar.isSelfAdjoint_iff_toMatrix'`, `Matrix.isSymm_iff_intrinsicStar_toLin'`, `WithConv.congr_apply`, `instSMulCommClassWithConvMatrix`, `TensorProduct.map_convMul_map`, `LinearMap.toSpanSingleton_convMul_toSpanSingleton`, `LinearMap.intrinsicStar_apply`, `LinearMap.isSelfAdjoint_iff_map_star`, `WithConv.toConv_injective`, `IntrinsicStar.StarHomClass.isSelfAdjoint`, `LinearMap.convMul_comp_coalgHom_distrib`, `intrinsicStar_def`, `WithConv.toConv_multisetSum`, `WithConv.symm_congrLinearEquiv_apply`, `Module.End.isUnit_intrinsicStar_iff`, `convMul_def`, `LinearMap.algHom_comp_convMul_distrib`, `WithConv.ofConv_multisetSum`, `WithConv.ofConv_smul`, `WithConv.ofConv_bijective`, `LinearMap.convMul_apply`, `WithConv.ofConv_add`, `StarHomClass.isSelfAdjoint`, `WithConv.symm_equiv_apply`, `WithConv.ofConv_sub`, `LinearMap.intrinsicStar_comp`, `WithConv.toConv_eq_zero`, `TensorProduct.star_map_apply_eq_map_intrinsicStar`, `WithConv.ofConv_neg`, `WithConv.ofConv_sum`, `ContinuousLinearMap.intrinsicStar_apply`, `WithConv.toConv_sum`, `WithConv.toConv_surjective`, `Module.End.IsUnit.intrinsicStar`, `WithConv.instNontrivial`, `ContinuousLinearMap.IntrinsicStar.isSelfAdjoint_toLinearMap_iff`, `LinearMap.intrinsicStar_eq_comp`, `WithConv.toAddEquiv_linearEquiv`
`instAlgebraWithConvMatrix` 📖	CompOp	2 math math: `WithConv.matrixToLin'StarAlgEquiv_apply`, `WithConv.symm_matrixToLin'StarAlgEquiv_apply`
`instCommMagmaWithConvMatrix` 📖	CompOp	—
`instCommMonoidWithConvMatrix` 📖	CompOp	—
`instCommRingWithConvMatrix` 📖	CompOp	—
`instCommSemiringWithConvMatrix` 📖	CompOp	—
`instInvolutiveStarWithConvMatrix` 📖	CompOp	—
`instMonoidWithConvMatrix` 📖	CompOp	—
`instMulOneClassWithConvMatrix` 📖	CompOp	—
`instMulWithConvMatrix` 📖	CompOp	5 math math: `WithConv.matrixToLin'StarAlgEquiv_apply`, `instIsScalarTowerWithConvMatrix`, `WithConv.symm_matrixToLin'StarAlgEquiv_apply`, `instSMulCommClassWithConvMatrix`, `convMul_def`
`instNonAssocCommRingWithConvMatrix` 📖	CompOp	—
`instNonAssocCommSemiringWithConvMatrix` 📖	CompOp	—
`instNonAssocRingWithConvMatrix` 📖	CompOp	—
`instNonAssocSemiringWithConvMatrix` 📖	CompOp	—
`instNonUnitalCommRingWithConvMatrix` 📖	CompOp	—
`instNonUnitalCommSemiringWithConvMatrix` 📖	CompOp	—
`instNonUnitalNonAssocCommRingWithConvMatrix` 📖	CompOp	—
`instNonUnitalNonAssocCommSemiringWithConvMatrix` 📖	CompOp	—
`instNonUnitalNonAssocRingWithConvMatrix` 📖	CompOp	—
`instNonUnitalNonAssocSemiringWithConvMatrix` 📖	CompOp	2 math math: `WithConv.matrixToLin'StarAlgEquiv_apply`, `WithConv.symm_matrixToLin'StarAlgEquiv_apply`
`instNonUnitalRingWithConvMatrix` 📖	CompOp	—
`instNonUnitalSemiringWithConvMatrix` 📖	CompOp	—
`instOneWithConvMatrix` 📖	CompOp	1 math math: `convOne_def`
`instRingWithConvMatrix` 📖	CompOp	—
`instSemigroupWithConvMatrix` 📖	CompOp	—
`instSemiringWithConvMatrix` 📖	CompOp	2 math math: `WithConv.matrixToLin'StarAlgEquiv_apply`, `WithConv.symm_matrixToLin'StarAlgEquiv_apply`
`instStarAddMonoidWithConvMatrix` 📖	CompOp	—
`instStarMulWithConvMatrix` 📖	CompOp	—
`instStarRingWithConvMatrix` 📖	CompOp	—
`instStarWithConvMatrix` 📖	CompOp	4 math math: `Matrix.WithConv.IsIdempotentElem.isSelfAdjoint`, `WithConv.matrixToLin'StarAlgEquiv_apply`, `WithConv.symm_matrixToLin'StarAlgEquiv_apply`, `intrinsicStar_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`convMul_def` 📖	mathematical	—	`WithConv` `Matrix` `instMulWithConvMatrix` `WithConv.toConv` `Matrix.hadamard` `WithConv.ofConv`	—	—
`convOne_def` 📖	mathematical	—	`WithConv` `Matrix` `instOneWithConvMatrix` `WithConv.toConv` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Matrix.of` `Pi.instOne`	—	—
`instIsScalarTowerWithConvMatrix` 📖	mathematical	—	`IsScalarTower` `WithConv` `Matrix` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `WithConv.instMulAction` `Matrix.mulAction` `instMulWithConvMatrix`	—	`Matrix.smul_hadamard`
`instSMulCommClassWithConvMatrix` 📖	mathematical	—	`SMulCommClass` `WithConv` `Matrix` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `WithConv.instMulAction` `Matrix.mulAction` `instMulWithConvMatrix`	—	`Matrix.hadamard_smul`
`intrinsicStar_def` 📖	mathematical	—	`Star.star` `WithConv` `Matrix` `instStarWithConvMatrix` `WithConv.toConv` `Matrix.map` `WithConv.ofConv`	—	—

---

← Back to Index