WithConv

📁 Source: Mathlib/Algebra/WithConv.lean

Statistics

Metric	Count
Definitions `addEquiv`, `congrLinearEquiv`, `delabToConv`, `equiv`, `instAddAction`, `instAddCommGroup`, `instAddCommMonoid`, `instAddGroup`, `instAddMonoid`, `instCoeFunForall`, `instDecidableEq`, `instDistribMulAction`, `instModule`, `instMulAction`, `instUnique`, `linearEquiv`, `ofConv`	17
Theorems `addEquiv_apply`, `addEquiv_symm_apply_ofConv`, `congrLinearEquiv_apply`, `congr_apply`, `equiv_apply`, `ext`, `ext_iff`, `instNontrivial`, `linearEquiv_apply`, `ofConv_add`, `ofConv_bijective`, `ofConv_eq_zero`, `ofConv_injective`, `ofConv_listSum`, `ofConv_multisetSum`, `ofConv_neg`, `ofConv_smul`, `ofConv_sub`, `ofConv_sum`, `ofConv_surjective`, `ofConv_toConv`, `ofConv_zero`, `symm_congr`, `symm_congrLinearEquiv`, `symm_congrLinearEquiv_apply`, `symm_congr_apply`, `symm_equiv_apply`, `symm_linearEquiv_apply`, `toAddEquiv_linearEquiv`, `toConv_add`, `toConv_bijective`, `toConv_eq_zero`, `toConv_injective`, `toConv_listSum`, `toConv_multisetSum`, `toConv_neg`, `toConv_ofConv`, `toConv_smul`, `toConv_sub`, `toConv_sum`, `toConv_surjective`, `toConv_zero`, `toEquiv_addEquiv`, `toEquiv_congrLinearEquiv`	44
Total	61

WithConv

Definitions

Name	Category	Theorems
`addEquiv` 📖	CompOp	4 math math: `addEquiv_symm_apply_ofConv`, `toEquiv_addEquiv`, `addEquiv_apply`, `toAddEquiv_linearEquiv`
`congrLinearEquiv` 📖	CompOp	4 math math: `congrLinearEquiv_apply`, `toEquiv_congrLinearEquiv`, `symm_congrLinearEquiv`, `symm_congrLinearEquiv_apply`
`delabToConv` 📖	CompOp	—
`equiv` 📖	CompOp	3 math math: `toEquiv_addEquiv`, `equiv_apply`, `symm_equiv_apply`
`instAddAction` 📖	CompOp	—
`instAddCommGroup` 📖	CompOp	—
`instAddCommMonoid` 📖	CompOp	14 math math: `ofConv_listSum`, `symm_linearEquiv_apply`, `LinearMap.IntrinsicStar.starLinearEquiv_eq_arrowCongr`, `congrLinearEquiv_apply`, `toEquiv_congrLinearEquiv`, `toConv_listSum`, `linearEquiv_apply`, `symm_congrLinearEquiv`, `toConv_multisetSum`, `symm_congrLinearEquiv_apply`, `ofConv_multisetSum`, `ofConv_sum`, `toConv_sum`, `toAddEquiv_linearEquiv`
`instAddGroup` 📖	CompOp	4 math math: `toConv_sub`, `toConv_neg`, `ofConv_sub`, `ofConv_neg`
`instAddMonoid` 📖	CompOp	15 math math: `ofConv_eq_zero`, `addEquiv_symm_apply_ofConv`, `toEquiv_addEquiv`, `ofConv_listSum`, `ofConv_zero`, `toConv_zero`, `LinearMap.intrinsicStar_zero`, `matrixToLin'StarAlgEquiv_apply`, `toConv_add`, `toConv_listSum`, `addEquiv_apply`, `LinearMap.intrinsicStarModule`, `symm_matrixToLin'StarAlgEquiv_apply`, `ofConv_add`, `toConv_eq_zero`
`instCoeFunForall` 📖	CompOp	—
`instDecidableEq` 📖	CompOp	—
`instDistribMulAction` 📖	CompOp	3 math math: `matrixToLin'StarAlgEquiv_apply`, `LinearMap.intrinsicStarModule`, `symm_matrixToLin'StarAlgEquiv_apply`
`instModule` 📖	CompOp	8 math math: `symm_linearEquiv_apply`, `LinearMap.IntrinsicStar.starLinearEquiv_eq_arrowCongr`, `congrLinearEquiv_apply`, `toEquiv_congrLinearEquiv`, `linearEquiv_apply`, `symm_congrLinearEquiv`, `symm_congrLinearEquiv_apply`, `toAddEquiv_linearEquiv`
`instMulAction` 📖	CompOp	5 math math: `ContinuousLinearMap.intrinsicStarModule`, `toConv_smul`, `instIsScalarTowerWithConvMatrix`, `instSMulCommClassWithConvMatrix`, `ofConv_smul`
`instUnique` 📖	CompOp	—
`linearEquiv` 📖	CompOp	4 math math: `symm_linearEquiv_apply`, `LinearMap.IntrinsicStar.starLinearEquiv_eq_arrowCongr`, `linearEquiv_apply`, `toAddEquiv_linearEquiv`
`ofConv` 📖	CompOp	61 math math: `ofConv_eq_zero`, `addEquiv_symm_apply_ofConv`, `LinearMap.convMul_def`, `Module.End.spectrum_intrinsicStar`, `ofConv_surjective`, `ofConv_listSum`, `ContinuousLinearMap.IntrinsicStar.isSelfAdjoint_iff_map_star`, `ofConv_injective`, `Matrix.toLin'_hadamard`, `Module.End.mem_eigenspace_intrinsicStar_iff`, `equiv_apply`, `LinearMap.convOne_apply`, `ofConv_zero`, `ContinuousLinearMap.intrinsicStar_comp`, `congrLinearEquiv_apply`, `matrixToLin'StarAlgEquiv_apply`, `ContinuousLinearMap.toLinearMap_intrinsicStar`, `symm_congr_apply`, `LinearMap.IntrinsicStar.isSelfAdjoint_iff_map_star`, `LinearMap.intrinsicStar_comp'`, `LinearMap.intrinsicStar_rTensor`, `TensorProduct.intrinsicStar_map`, `ofConv_toConv`, `ContinuousLinearMap.intrinsicStar_eq_comp`, `LinearMap.toMatrix'_intrinsicStar`, `linearEquiv_apply`, `Coalgebra.Repr.convMul_apply`, `addEquiv_apply`, `ContinuousLinearMap.intrinsicStar_smulRight`, `LinearMap.nonUnitalAlgHom_comp_convMul_distrib`, `LinearMap.intrinsicStar_lTensor`, `LinearMap.intrinsicStar_smulRight`, `ContinuousLinearMap.intrinsicStar_comp'`, `symm_matrixToLin'StarAlgEquiv_apply`, `toConv_ofConv`, `LinearMap.IntrinsicStar.isSelfAdjoint_iff_toMatrix'`, `congr_apply`, `TensorProduct.map_convMul_map`, `LinearMap.intrinsicStar_apply`, `LinearMap.isSelfAdjoint_iff_map_star`, `LinearMap.convMul_comp_coalgHom_distrib`, `intrinsicStar_def`, `symm_congrLinearEquiv_apply`, `Module.End.isUnit_intrinsicStar_iff`, `convMul_def`, `LinearMap.algHom_comp_convMul_distrib`, `ofConv_multisetSum`, `ofConv_smul`, `ofConv_bijective`, `LinearMap.convMul_apply`, `ofConv_add`, `ext_iff`, `ofConv_sub`, `LinearMap.intrinsicStar_comp`, `TensorProduct.star_map_apply_eq_map_intrinsicStar`, `ofConv_neg`, `ofConv_sum`, `ContinuousLinearMap.intrinsicStar_apply`, `Module.End.IsUnit.intrinsicStar`, `ContinuousLinearMap.IntrinsicStar.isSelfAdjoint_toLinearMap_iff`, `LinearMap.intrinsicStar_eq_comp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `WithConv` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `instAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `addEquiv` `ofConv`	—	—
`addEquiv_symm_apply_ofConv` 📖	mathematical	—	`ofConv` `DFunLike.coe` `AddEquiv` `WithConv` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `instAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `addEquiv`	—	—
`congrLinearEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `WithConv` `instAddCommMonoid` `instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `congrLinearEquiv` `toConv` `ofConv`	—	`RingHomInvPair.ids`
`congr_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `WithConv` `EquivLike.toFunLike` `Equiv.instEquivLike` `congr` `toConv` `ofConv`	—	—
`equiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `WithConv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `ofConv`	—	—
`ext` 📖	—	`ofConv`	—	—	`ofConv_injective`
`ext_iff` 📖	mathematical	—	`ofConv`	—	`ext`
`instNontrivial` 📖	mathematical	—	`Nontrivial` `WithConv`	—	`Equiv.nontrivial`
`linearEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `WithConv` `instAddCommMonoid` `instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `linearEquiv` `ofConv`	—	`RingHomInvPair.ids`
`ofConv_add` 📖	mathematical	—	`ofConv` `WithConv` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `instAddMonoid`	—	—
`ofConv_bijective` 📖	mathematical	—	`Function.Bijective` `WithConv` `ofConv`	—	`ofConv_injective` `ofConv_surjective`
`ofConv_eq_zero` 📖	mathematical	—	`ofConv` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `WithConv` `instAddMonoid`	—	`ofConv_injective`
`ofConv_injective` 📖	mathematical	—	`WithConv` `ofConv`	—	`toConv_ofConv`
`ofConv_listSum` 📖	mathematical	—	`ofConv` `WithConv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoid` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddMonoid` `AddCommMonoid.toAddMonoid`	—	`map_list_sum` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`ofConv_multisetSum` 📖	mathematical	—	`ofConv` `Multiset.sum` `WithConv` `instAddCommMonoid` `Multiset.map`	—	`map_multiset_sum` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`ofConv_neg` 📖	mathematical	—	`ofConv` `WithConv` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `instAddGroup`	—	—
`ofConv_smul` 📖	mathematical	—	`ofConv` `WithConv` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `instMulAction`	—	—
`ofConv_sub` 📖	mathematical	—	`ofConv` `WithConv` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `instAddGroup`	—	—
`ofConv_sum` 📖	mathematical	—	`ofConv` `Finset.sum` `WithConv` `instAddCommMonoid`	—	`map_sum` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`ofConv_surjective` 📖	mathematical	—	`WithConv` `ofConv`	—	`ofConv_toConv`
`ofConv_toConv` 📖	mathematical	—	`ofConv` `toConv`	—	—
`ofConv_zero` 📖	mathematical	—	`ofConv` `WithConv` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddMonoid`	—	—
`symm_congr` 📖	mathematical	—	`Equiv.symm` `WithConv` `congr`	—	—
`symm_congrLinearEquiv` 📖	mathematical	—	`LinearEquiv.symm` `WithConv` `instAddCommMonoid` `instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `congrLinearEquiv`	—	`RingHomInvPair.ids`
`symm_congrLinearEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `WithConv` `instAddCommMonoid` `instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `congrLinearEquiv` `toConv` `ofConv`	—	`RingHomInvPair.ids`
`symm_congr_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `WithConv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `congr` `toConv` `ofConv`	—	—
`symm_equiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `WithConv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equiv` `toConv`	—	—
`symm_linearEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `WithConv` `instAddCommMonoid` `instModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `linearEquiv` `toConv`	—	`RingHomInvPair.ids`
`toAddEquiv_linearEquiv` 📖	mathematical	—	`LinearEquiv.toAddEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `WithConv` `instAddCommMonoid` `instModule` `linearEquiv` `addEquiv` `AddCommMonoid.toAddMonoid`	—	`RingHomInvPair.ids`
`toConv_add` 📖	mathematical	—	`toConv` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `WithConv` `instAddMonoid`	—	—
`toConv_bijective` 📖	mathematical	—	`Function.Bijective` `WithConv` `toConv`	—	`toConv_injective` `toConv_surjective`
`toConv_eq_zero` 📖	mathematical	—	`toConv` `WithConv` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddMonoid`	—	`toConv_injective`
`toConv_injective` 📖	mathematical	—	`WithConv` `toConv`	—	`ofConv_toConv`
`toConv_listSum` 📖	mathematical	—	`toConv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `WithConv` `instAddCommMonoid` `instAddMonoid`	—	`map_list_sum` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`toConv_multisetSum` 📖	mathematical	—	`toConv` `Multiset.sum` `WithConv` `instAddCommMonoid` `Multiset.map`	—	`map_multiset_sum` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`toConv_neg` 📖	mathematical	—	`toConv` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `WithConv` `instAddGroup`	—	—
`toConv_ofConv` 📖	mathematical	—	`toConv` `ofConv`	—	—
`toConv_smul` 📖	mathematical	—	`toConv` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `WithConv` `instMulAction`	—	—
`toConv_sub` 📖	mathematical	—	`toConv` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `WithConv` `instAddGroup`	—	—
`toConv_sum` 📖	mathematical	—	`toConv` `Finset.sum` `WithConv` `instAddCommMonoid`	—	`map_sum` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`toConv_surjective` 📖	mathematical	—	`WithConv` `toConv`	—	`toConv_ofConv`
`toConv_zero` 📖	mathematical	—	`toConv` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `WithConv` `instAddMonoid`	—	—
`toEquiv_addEquiv` 📖	mathematical	—	`EquivLike.toEquiv` `WithConv` `AddEquiv` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `instAddMonoid` `AddEquiv.instEquivLike` `addEquiv` `equiv`	—	—
`toEquiv_congrLinearEquiv` 📖	mathematical	—	`LinearEquiv.toEquiv` `WithConv` `instAddCommMonoid` `instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `congrLinearEquiv` `congr`	—	`RingHomInvPair.ids`

---

← Back to Index