Documentation Verification Report

Matrix

📁 Source: Mathlib/Analysis/Normed/Lp/Matrix.lean

Statistics

Metric	Count
Definitions `toLpLin`, `toLpLinAlgEquiv`	2
Theorems `ofLp_toLpLin`, `toLpLinAlgEquiv_apply_apply_ofLp`, `toLpLinAlgEquiv_symm_apply`, `toLpLin_apply`, `toLpLin_eq_toLin`, `toLpLin_mul`, `toLpLin_mul_same`, `toLpLin_one`, `toLpLin_pow`, `toLpLin_symm_comp`, `toLpLin_symm_id`, `toLpLin_symm_pow`, `toLpLin_toLp`	13
Total	15

Matrix

Definitions

Name	Category	Theorems
`toLpLin` 📖	CompOp	13 math math: `spectrum_toLpLin`, `toLpLin_mul_same`, `toLpLin_symm_pow`, `toLpLin_one`, `toLpLin_pow`, `ofLp_toLpLin`, `toLpLin_toLp`, `toLpLin_symm_id`, `toLpLin_mul`, `toLpLin_symm_comp`, `toLpLin_apply`, `toLpLinAlgEquiv_symm_apply`, `toLpLin_eq_toLin`
`toLpLinAlgEquiv` 📖	CompOp	2 math math: `toLpLinAlgEquiv_apply_apply_ofLp`, `toLpLinAlgEquiv_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofLp_toLpLin` 📖	mathematical	—	`WithLp.ofLp` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `WithLp` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `WithLp.instModule` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Semiring.toModule` `LinearMap.instFunLike` `LinearEquiv` `RingHomInvPair.ids` `Matrix` `addCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LinearMap.addCommMonoid` `module` `LinearMap.module` `WithLp.instSMulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction` `Function.smulCommClass` `AddCommMonoid.toAddMonoid` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toLpLin` `Pi.addCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `toLin'`	—	`RingHomInvPair.ids` `WithLp.instSMulCommClass` `Function.smulCommClass` `Algebra.to_smulCommClass`
`toLpLinAlgEquiv_apply_apply_ofLp` 📖	mathematical	—	`WithLp.ofLp` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `WithLp` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `WithLp.instModule` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Semiring.toModule` `LinearMap.instFunLike` `AlgEquiv` `Matrix` `Module.End` `semiring` `Module.End.instSemiring` `instAlgebra` `Algebra.id` `Module.End.instAlgebra` `WithLp.instSMulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction` `Function.smulCommClass` `AddCommMonoid.toAddMonoid` `Algebra.to_smulCommClass` `Algebra.toSMul` `WithLp.instIsScalarTower` `Pi.isScalarTower` `IsScalarTower.right` `AlgEquiv.instFunLike` `toLpLinAlgEquiv` `mulVec` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`WithLp.instSMulCommClass` `Function.smulCommClass` `Algebra.to_smulCommClass` `WithLp.instIsScalarTower` `Pi.isScalarTower` `IsScalarTower.right`
`toLpLinAlgEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Module.End` `WithLp` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `WithLp.instModule` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Semiring.toModule` `Matrix` `Module.End.instSemiring` `semiring` `Module.End.instAlgebra` `WithLp.instSMulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction` `Function.smulCommClass` `AddCommMonoid.toAddMonoid` `Algebra.to_smulCommClass` `Algebra.id` `Algebra.toSMul` `WithLp.instIsScalarTower` `Pi.isScalarTower` `IsScalarTower.right` `instAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `toLpLinAlgEquiv` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `toLpLin`	—	`WithLp.instSMulCommClass` `Function.smulCommClass` `Algebra.to_smulCommClass` `WithLp.instIsScalarTower` `Pi.isScalarTower` `IsScalarTower.right`
`toLpLin_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `WithLp` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `WithLp.instModule` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Semiring.toModule` `LinearMap.instFunLike` `LinearEquiv` `RingHomInvPair.ids` `Matrix` `addCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LinearMap.addCommMonoid` `module` `LinearMap.module` `WithLp.instSMulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction` `Function.smulCommClass` `AddCommMonoid.toAddMonoid` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toLpLin` `WithLp.toLp` `mulVec` `WithLp.ofLp`	—	`RingHomInvPair.ids` `WithLp.instSMulCommClass` `Function.smulCommClass` `Algebra.to_smulCommClass`
`toLpLin_eq_toLin` 📖	mathematical	—	`toLpLin` `toLin` `CommRing.toCommSemiring` `PiLp` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `WithLp.instModule` `Ring.toSemiring` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `PiLp.basisFun` `Finite.of_fintype`	—	`RingHomInvPair.ids` `WithLp.instSMulCommClass` `Function.smulCommClass` `Algebra.to_smulCommClass`
`toLpLin_mul` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Matrix` `LinearMap` `WithLp` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `WithLp.instModule` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Semiring.toModule` `addCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LinearMap.addCommMonoid` `module` `LinearMap.module` `WithLp.instSMulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction` `Function.smulCommClass` `AddCommMonoid.toAddMonoid` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toLpLin` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `LinearMap.comp` `RingHomCompTriple.ids`	—	`LinearMap.ext` `RingHomInvPair.ids` `WithLp.instSMulCommClass` `Function.smulCommClass` `Algebra.to_smulCommClass` `RingHomCompTriple.ids` `PiLp.ext` `toLin'_mul` `mulVec_mulVec`
`toLpLin_mul_same` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Matrix` `LinearMap` `WithLp` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `WithLp.instModule` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Semiring.toModule` `addCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LinearMap.addCommMonoid` `module` `LinearMap.module` `WithLp.instSMulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction` `Function.smulCommClass` `AddCommMonoid.toAddMonoid` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toLpLin` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `LinearMap.comp` `RingHomCompTriple.ids`	—	`toLpLin_mul`
`toLpLin_one` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Matrix` `LinearMap` `WithLp` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `WithLp.instModule` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Semiring.toModule` `addCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LinearMap.addCommMonoid` `module` `LinearMap.module` `WithLp.instSMulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction` `Function.smulCommClass` `AddCommMonoid.toAddMonoid` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toLpLin` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `LinearMap.id`	—	`LinearMap.ext` `RingHomInvPair.ids` `WithLp.instSMulCommClass` `Function.smulCommClass` `Algebra.to_smulCommClass` `PiLp.ext` `toLin'_one`
`toLpLin_pow` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Matrix` `LinearMap` `WithLp` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `WithLp.instModule` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Semiring.toModule` `addCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LinearMap.addCommMonoid` `module` `LinearMap.module` `WithLp.instSMulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction` `Function.smulCommClass` `AddCommMonoid.toAddMonoid` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toLpLin` `Monoid.toNatPow` `semiring` `Module.End.instMonoid`	—	`map_pow` `WithLp.instSMulCommClass` `Function.smulCommClass` `Algebra.to_smulCommClass` `WithLp.instIsScalarTower` `Pi.isScalarTower` `IsScalarTower.right` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass`
`toLpLin_symm_comp` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearMap` `WithLp` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `WithLp.instModule` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Semiring.toModule` `Matrix` `LinearMap.addCommMonoid` `addCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LinearMap.module` `WithLp.instSMulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction` `Function.smulCommClass` `AddCommMonoid.toAddMonoid` `Algebra.to_smulCommClass` `Algebra.id` `module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `toLpLin` `LinearMap.comp` `RingHomCompTriple.ids` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`LinearEquiv.injective` `WithLp.instSMulCommClass` `Function.smulCommClass` `Algebra.to_smulCommClass` `RingHomInvPair.ids` `RingHomCompTriple.ids` `LinearEquiv.apply_symm_apply` `toLpLin_mul` `LinearMap.comp.congr_simp`
`toLpLin_symm_id` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearMap` `WithLp` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `WithLp.instModule` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Semiring.toModule` `Matrix` `LinearMap.addCommMonoid` `addCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LinearMap.module` `WithLp.instSMulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction` `Function.smulCommClass` `AddCommMonoid.toAddMonoid` `Algebra.to_smulCommClass` `Algebra.id` `module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `toLpLin` `LinearMap.id` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`LinearEquiv.injective` `WithLp.instSMulCommClass` `Function.smulCommClass` `Algebra.to_smulCommClass` `RingHomInvPair.ids` `LinearEquiv.apply_symm_apply` `toLpLin_one`
`toLpLin_symm_pow` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearMap` `WithLp` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `WithLp.instModule` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Semiring.toModule` `Matrix` `LinearMap.addCommMonoid` `addCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LinearMap.module` `WithLp.instSMulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction` `Function.smulCommClass` `AddCommMonoid.toAddMonoid` `Algebra.to_smulCommClass` `Algebra.id` `module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `toLpLin` `Module.End` `Monoid.toNatPow` `Module.End.instMonoid` `semiring`	—	`map_pow` `WithLp.instSMulCommClass` `Function.smulCommClass` `Algebra.to_smulCommClass` `WithLp.instIsScalarTower` `Pi.isScalarTower` `IsScalarTower.right` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass`
`toLpLin_toLp` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `WithLp` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `WithLp.instModule` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Semiring.toModule` `LinearMap.instFunLike` `LinearEquiv` `RingHomInvPair.ids` `Matrix` `addCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `LinearMap.addCommMonoid` `module` `LinearMap.module` `WithLp.instSMulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction` `Function.smulCommClass` `AddCommMonoid.toAddMonoid` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toLpLin` `WithLp.toLp` `Pi.addCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `toLin'`	—	`RingHomInvPair.ids` `WithLp.instSMulCommClass` `Function.smulCommClass` `Algebra.to_smulCommClass`

---

← Back to Index