WithConv

📁 Source: Mathlib/Algebra/WithConv.lean

Statistics

Metric	Count
Definitions `WithConv`, `addEquiv`, `delabToConv`, `equiv`, `instAddAction`, `instAddCommGroup`, `instAddCommMonoid`, `instAddGroup`, `instAddMonoid`, `instCoeFunForall`, `instDecidableEq`, `instDistribMulAction`, `instModule`, `instMulAction`, `instUnique`, `linearEquiv`, `ofConv`	17
Theorems `addEquiv_apply`, `addEquiv_symm_apply_ofConv`, `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_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`	37
Total	54

WithConv

Definitions

Name	Category	Theorems
`addEquiv` 📖	CompOp	4 math math: `addEquiv_symm_apply_ofConv`, `toEquiv_addEquiv`, `addEquiv_apply`, `toAddEquiv_linearEquiv`
`delabToConv` 📖	CompOp	—
`equiv` 📖	CompOp	3 math math: `toEquiv_addEquiv`, `equiv_apply`, `symm_equiv_apply`
`instAddAction` 📖	CompOp	—
`instAddCommGroup` 📖	CompOp	—
`instAddCommMonoid` 📖	CompOp	10 math math: `ofConv_listSum`, `symm_linearEquiv_apply`, `LinearMap.IntrinsicStar.starLinearEquiv_eq_arrowCongr`, `toConv_listSum`, `linearEquiv_apply`, `toConv_multisetSum`, `ofConv_multisetSum`, `ofConv_sum`, `toConv_sum`, `toAddEquiv_linearEquiv`
`instAddGroup` 📖	CompOp	4 math math: `toConv_sub`, `toConv_neg`, `ofConv_sub`, `ofConv_neg`
`instAddMonoid` 📖	CompOp	13 math math: `ofConv_eq_zero`, `addEquiv_symm_apply_ofConv`, `toEquiv_addEquiv`, `ofConv_listSum`, `ofConv_zero`, `toConv_zero`, `LinearMap.intrinsicStar_zero`, `toConv_add`, `toConv_listSum`, `addEquiv_apply`, `LinearMap.intrinsicStarModule`, `ofConv_add`, `toConv_eq_zero`
`instCoeFunForall` 📖	CompOp	—
`instDecidableEq` 📖	CompOp	—
`instDistribMulAction` 📖	CompOp	1 math math: `LinearMap.intrinsicStarModule`
`instModule` 📖	CompOp	4 math math: `symm_linearEquiv_apply`, `LinearMap.IntrinsicStar.starLinearEquiv_eq_arrowCongr`, `linearEquiv_apply`, `toAddEquiv_linearEquiv`
`instMulAction` 📖	CompOp	2 math math: `toConv_smul`, `ofConv_smul`
`instUnique` 📖	CompOp	—
`linearEquiv` 📖	CompOp	4 math math: `symm_linearEquiv_apply`, `LinearMap.IntrinsicStar.starLinearEquiv_eq_arrowCongr`, `linearEquiv_apply`, `toAddEquiv_linearEquiv`
`ofConv` 📖	CompOp	43 math math: `ofConv_eq_zero`, `addEquiv_symm_apply_ofConv`, `LinearMap.convMul_def`, `Module.End.spectrum_intrinsicStar`, `ofConv_surjective`, `ofConv_listSum`, `ofConv_injective`, `Module.End.mem_eigenspace_intrinsicStar_iff`, `equiv_apply`, `LinearMap.convOne_apply`, `ofConv_zero`, `LinearMap.IntrinsicStar.isSelfAdjoint_iff_map_star`, `LinearMap.intrinsicStar_comp'`, `LinearMap.intrinsicStar_rTensor`, `TensorProduct.intrinsicStar_map`, `ofConv_toConv`, `LinearMap.toMatrix'_intrinsicStar`, `linearEquiv_apply`, `Coalgebra.Repr.convMul_apply`, `addEquiv_apply`, `LinearMap.nonUnitalAlgHom_comp_convMul_distrib`, `LinearMap.intrinsicStar_lTensor`, `LinearMap.intrinsicStar_smulRight`, `toConv_ofConv`, `LinearMap.IntrinsicStar.isSelfAdjoint_iff_toMatrix'`, `TensorProduct.map_convMul_map`, `LinearMap.intrinsicStar_apply`, `LinearMap.isSelfAdjoint_iff_map_star`, `LinearMap.convMul_comp_coalgHom_distrib`, `Module.End.isUnit_intrinsicStar_iff`, `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`, `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`	—	—
`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_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`	—	—

(root)

Definitions

Name	Category	Theorems
`WithConv` 📖	CompData	74 math math: `WithConv.ofConv_eq_zero`, `WithConv.addEquiv_symm_apply_ofConv`, `LinearMap.convMul_def`, `WithConv.toConv_bijective`, `WithConv.toEquiv_addEquiv`, `LinearMap.intrinsicStar_mulRight`, `Module.End.spectrum_intrinsicStar`, `WithConv.ofConv_surjective`, `WithConv.ofConv_listSum`, `Matrix.intrinsicStar_toLin'`, `LinearMap.intrinsicStar_toSpanSingleton`, `WithConv.ofConv_injective`, `WithConv.symm_linearEquiv_apply`, `Module.End.mem_eigenspace_intrinsicStar_iff`, `WithConv.equiv_apply`, `LinearMap.convOne_apply`, `Pi.intrinsicStar_comul_commSemiring`, `WithConv.toConv_sub`, `WithConv.toConv_smul`, `LinearMap.intrinsicStar_mul'`, `WithConv.ofConv_zero`, `WithConv.toConv_zero`, `LinearMap.IntrinsicStar.starLinearEquiv_eq_arrowCongr`, `LinearMap.intrinsicStar_zero`, `LinearMap.IntrinsicStar.isSelfAdjoint_iff_map_star`, `LinearMap.intrinsicStar_comp'`, `LinearMap.intrinsicStar_rTensor`, `TensorProduct.intrinsicStar_map`, `Matrix.IntrinsicStar.isSelfAdjoint_toLin'_iff`, `LinearMap.toMatrix'_intrinsicStar`, `WithConv.toConv_add`, `LinearMap.convOne_def`, `WithConv.toConv_listSum`, `WithConv.linearEquiv_apply`, `WithConv.toConv_neg`, `LinearMap.intrinsicStar_id`, `Coalgebra.Repr.convMul_apply`, `WithConv.addEquiv_apply`, `LinearMap.intrinsicStar_mulLeft`, `LinearMap.nonUnitalAlgHom_comp_convMul_distrib`, `LinearMap.intrinsicStar_lTensor`, `LinearMap.intrinsicStarModule`, `LinearMap.intrinsicStar_single`, `LinearMap.intrinsicStar_smulRight`, `LinearMap.IntrinsicStar.isSelfAdjoint_iff_toMatrix'`, `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`, `WithConv.toConv_multisetSum`, `Module.End.isUnit_intrinsicStar_iff`, `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`, `WithConv.toConv_sum`, `WithConv.toConv_surjective`, `Module.End.IsUnit.intrinsicStar`, `WithConv.instNontrivial`, `LinearMap.intrinsicStar_eq_comp`, `WithConv.toAddEquiv_linearEquiv`

---

← Back to Index