Documentation Verification Report

LinearMap

📁 Source: Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean

Statistics

Metric	Count
Definitions `isRepresentation`, `toEnd`, `fromEnd`, `fromMatrix`	4
Theorems `exists_monic_and_aeval_eq_zero`, `exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul`, `add`, `algebraMap`, `congr_fun`, `eq`, `mul`, `one`, `smul`, `zero`, `eq_toEnd_of_represents`, `toEnd_exists_mem_ideal`, `toEnd_represents`, `toEnd_surjective`, `represents_iff`, `represents_iff'`, `fromEnd_apply`, `fromEnd_apply_single_one`, `fromEnd_injective`, `fromMatrix_apply`, `fromMatrix_apply_single_one`	21
Total	25

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_monic_and_aeval_eq_zero` 📖	mathematical	—	`Polynomial.Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `Module.End` `AddCommGroup.toAddCommMonoid` `Polynomial.semiring` `Module.End.instSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgHom.funLike` `Polynomial.aeval` `instZero` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`IsScalarTower.right` `smulCommClass_self` `IsScalarTower.left` `exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul` `RingHomSurjective.ids` `Submodule.top_smul`
`exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Ideal` `Submodule.instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Top.top` `Submodule.instTop`	`Polynomial.Monic` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `Polynomial.natDegree` `Polynomial.coeff` `DFunLike.coe` `AlgHom` `Polynomial` `Module.End` `Polynomial.semiring` `Module.End.instSemiring` `Polynomial.algebraOfAlgebra` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `AlgHom.funLike` `Polynomial.aeval` `instZero`	—	`RingHomSurjective.ids` `IsScalarTower.left` `subsingleton_or_nontrivial` `IsScalarTower.right` `smulCommClass_self` `Polynomial.monic_of_subsingleton` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pow_zero` `Ideal.one_eq_top` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Module.Finite.fg_top` `Subtype.range_coe_subtype` `Finset.setOf_mem` `Matrix.isRepresentation.toEnd_exists_mem_ideal` `Matrix.charpoly_monic` `Matrix.charpoly_natDegree_eq_dim` `Matrix.coeff_charpoly_mem_ideal_pow` `Polynomial.aeval_algHom_apply` `Polynomial.aeval_subalgebra_coe` `Matrix.aeval_self_charpoly` `SubsemiringClass.toAddSubmonoidClass` `Subalgebra.instSubsemiringClass` `Subalgebra.coe_zero`

Matrix

Definitions

Name	Category	Theorems
`isRepresentation` 📖	CompOp	3 math math: `isRepresentation.toEnd_represents`, `isRepresentation.toEnd_exists_mem_ideal`, `isRepresentation.toEnd_surjective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`represents_iff` 📖	mathematical	—	`Represents` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `Fintype.linearCombination` `mulVec` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.End`	—	`Represents.congr_fun` `LinearMap.ext`
`represents_iff'` 📖	mathematical	—	`Represents` `Finset.sum` `AddCommGroup.toAddCommMonoid` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `DFunLike.coe` `Module.End` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`LinearMap.congr_fun` `smulCommClass_self` `PiToModule.fromMatrix_apply_single_one` `PiToModule.fromEnd_apply_single_one` `LinearMap.pi_ext'` `Finite.of_fintype` `LinearMap.ext_ring` `RingHomCompTriple.ids`

Matrix.Represents

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`Matrix.Represents`	`Matrix` `Matrix.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instAdd` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass`
`algebraMap` 📖	mathematical	—	`Matrix.Represents` `DFunLike.coe` `RingHom` `Matrix` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Matrix.semiring` `RingHom.instFunLike` `algebraMap` `Matrix.instAlgebra` `Algebra.id` `Module.End` `AddCommGroup.toAddCommMonoid` `Module.End.instSemiring` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`smulCommClass_self` `IsScalarTower.left` `congr_simp` `Algebra.algebraMap_eq_smul_one` `smul` `one`
`congr_fun` 📖	mathematical	`Matrix.Represents`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `Fintype.linearCombination` `Matrix.mulVec` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.End`	—	`LinearMap.congr_fun`
`eq` 📖	—	`Submodule.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Set.range` `Top.top` `Submodule` `Submodule.instTop` `Matrix.Represents`	—	—	`PiToModule.fromEnd_injective` `smulCommClass_self`
`mul` 📖	mathematical	`Matrix.Represents`	`Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMul`	—	`LinearMap.comp_apply` `AlgEquiv.toLinearMap_apply` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `LinearMap.pi_ext'` `Finite.of_fintype` `LinearMap.ext_ring` `RingHomCompTriple.ids` `congr_fun`
`one` 📖	mathematical	—	`Matrix.Represents` `Matrix` `Matrix.one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instOne`	—	`LinearMap.comp_apply` `AlgEquiv.toLinearMap_apply` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `LinearMap.pi_ext'` `Finite.of_fintype` `LinearMap.ext_ring` `RingHomCompTriple.ids`
`smul` 📖	mathematical	`Matrix.Represents`	`Matrix` `Matrix.smul` `Algebra.toSMul` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Module.End` `AddCommGroup.toAddCommMonoid` `LinearMap.instSMul` `RingHom.id` `Semiring.toNonAssocSemiring` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing`	—	`smulCommClass_self` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`zero` 📖	mathematical	—	`Matrix.Represents` `Matrix` `Matrix.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instZero` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`

Matrix.isRepresentation

Definitions

Name	Category	Theorems
`toEnd` 📖	CompOp	4 math math: `toEnd_represents`, `toEnd_exists_mem_ideal`, `toEnd_surjective`, `eq_toEnd_of_represents`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_toEnd_of_represents` 📖	mathematical	`Submodule.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Set.range` `Top.top` `Submodule` `Submodule.instTop` `Matrix.Represents` `Matrix` `Subalgebra` `Matrix.semiring` `Matrix.instAlgebra` `Algebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `Matrix.isRepresentation`	`DFunLike.coe` `AlgHom` `Module.End` `Subalgebra.toSemiring` `Module.End.instSemiring` `Subalgebra.algebra` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgHom.funLike` `toEnd`	—	`Matrix.Represents.eq`
`toEnd_exists_mem_ideal` 📖	mathematical	`Submodule.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Set.range` `Top.top` `Submodule` `Submodule.instTop` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Ideal` `Submodule.instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	`DFunLike.coe` `AlgHom` `Matrix` `Subalgebra` `Matrix.semiring` `Matrix.instAlgebra` `Algebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `Matrix.isRepresentation` `Module.End` `Subalgebra.toSemiring` `Module.End.instSemiring` `Subalgebra.algebra` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `AlgHom.funLike` `toEnd` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`RingHomSurjective.ids` `IsScalarTower.left` `Ideal.range_finsuppTotal` `LinearMap.mem_range_self` `Matrix.represents_iff'` `Ideal.finsuppTotal_apply_eq_of_fintype` `smulCommClass_self` `eq_toEnd_of_represents` `Subtype.prop`
`toEnd_represents` 📖	mathematical	`Submodule.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Set.range` `Top.top` `Submodule` `Submodule.instTop`	`Matrix.Represents` `Matrix` `Subalgebra` `Matrix.semiring` `Matrix.instAlgebra` `Algebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `Matrix.isRepresentation` `DFunLike.coe` `AlgHom` `Module.End` `Subalgebra.toSemiring` `Module.End.instSemiring` `Subalgebra.algebra` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgHom.funLike` `toEnd`	—	—
`toEnd_surjective` 📖	mathematical	`Submodule.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Set.range` `Top.top` `Submodule` `Submodule.instTop`	`Matrix` `Subalgebra` `Matrix.semiring` `Matrix.instAlgebra` `Algebra.id` `SetLike.instMembership` `Subalgebra.instSetLike` `Matrix.isRepresentation` `Module.End` `DFunLike.coe` `AlgHom` `Subalgebra.toSemiring` `Module.End.instSemiring` `Subalgebra.algebra` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgHom.funLike` `toEnd`	—	`smulCommClass_self` `IsScalarTower.left` `toEnd_exists_mem_ideal` `RingHomSurjective.ids` `Submodule.top_smul`

PiToModule

Definitions

Name	Category	Theorems
`fromEnd` 📖	CompOp	3 math math: `fromEnd_apply`, `fromEnd_injective`, `fromEnd_apply_single_one`
`fromMatrix` 📖	CompOp	2 math math: `fromMatrix_apply_single_one`, `fromMatrix_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fromEnd_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `Module.End` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `fromEnd` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Fintype.linearCombination`	—	`smulCommClass_self`
`fromEnd_apply_single_one` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `Module.End` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `fromEnd` `Pi.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`smulCommClass_self` `fromEnd_apply` `Fintype.linearCombination_apply_single` `one_smul`
`fromEnd_injective` 📖	mathematical	`Submodule.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Set.range` `Top.top` `Submodule` `Submodule.instTop`	`Module.End` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `Semiring.toModule` `DFunLike.coe` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `LinearMap.instFunLike` `fromEnd`	—	`smulCommClass_self` `LinearMap.ext` `RingHomSurjective.ids` `Fintype.range_linearCombination` `Submodule.mem_top` `LinearMap.congr_fun`
`fromMatrix_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `Matrix` `Matrix.addCommMonoid` `LinearMap.addCommMonoid` `Matrix.module` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `fromMatrix` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Fintype.linearCombination` `Matrix.mulVec`	—	`smulCommClass_self`
`fromMatrix_apply_single_one` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `Matrix` `Matrix.addCommMonoid` `LinearMap.addCommMonoid` `Matrix.module` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `fromMatrix` `Pi.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Finset.sum` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`smulCommClass_self` `fromMatrix_apply` `Fintype.linearCombination_apply` `Matrix.mulVec_single` `Finset.sum_congr` `one_smul`

---

← Back to Index