LSum

📁 Source: Mathlib/LinearAlgebra/Finsupp/LSum.lean

Statistics

Metric	Count
Definitions `domLCongr`, `lcongr`, `llift`, `lsum`, `splittingOfFinsuppSurjective`, `mulLeftMap`, `mulRightMap`	7
Theorems `coe_lsum`, `domLCongr_apply`, `domLCongr_refl`, `domLCongr_single`, `domLCongr_symm`, `domLCongr_trans`, `lcongr_apply_apply`, `lcongr_single`, `lcongr_symm`, `lcongr_symm_single`, `lift_apply`, `lift_symm_apply`, `llift_apply`, `llift_symm_apply`, `lsum_apply`, `lsum_comp_lsingle`, `lsum_single`, `lsum_symm_apply`, `smul_sum`, `sum_smul_index_linearMap'`, `sum_smul_index_semilinearMap'`, `finsupp_cod`, `finsupp_dom`, `coe_finsupp_sum`, `finsupp_sum_apply`, `leftInverse_splittingOfFinsuppSurjective`, `splittingOfFinsuppSurjective_injective`, `splittingOfFinsuppSurjective_splits`, `finsuppSum_mem`, `mulLeftMap_apply`, `mulLeftMap_apply_single`, `mulLeftMap_eq_mulRightMap`, `mulLeftMap_eq_mulRightMap_of_commute`, `mulRightMap_apply`, `mulRightMap_apply_single`	35
Total	42

Finsupp

Definitions

Name	Category	Theorems
`domLCongr` 📖	CompOp	9 math math: `domLCongr_trans`, `Rep.diagonalOneIsoLeftRegular_inv_hom`, `domLCongr_symm`, `Rep.leftRegularTensorTrivialIsoFree_inv_hom`, `domLCongr_apply`, `Rep.diagonalOneIsoLeftRegular_hom_hom`, `Rep.leftRegularTensorTrivialIsoFree_hom_hom`, `domLCongr_refl`, `domLCongr_single`
`lcongr` 📖	CompOp	4 math math: `lcongr_symm`, `lcongr_symm_single`, `lcongr_single`, `lcongr_apply_apply`
`llift` 📖	CompOp	2 math math: `llift_apply`, `llift_symm_apply`
`lsum` 📖	CompOp	11 math math: `Representation.finsupp_apply`, `TensorProduct.sum_tmul_basis_right_injective`, `TensorProduct.equivFinsuppOfBasisLeft_symm`, `lsum_single`, `Submodule.set_smul_eq_map`, `lsum_apply`, `coe_lsum`, `lsum_comp_lsingle`, `TensorProduct.equivFinsuppOfBasisRight_symm`, `TensorProduct.sum_tmul_basis_left_injective`, `lsum_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_lsum` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `module` `LinearMap.instFunLike` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Pi.addCommMonoid` `LinearMap.addCommMonoid` `Pi.Function.module` `LinearMap.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `lsum` `sum`	—	`RingHomInvPair.ids`
`domLCongr_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `domLCongr` `AddEquiv` `instAdd` `AddEquiv.instEquivLike` `domCongr`	—	`RingHomInvPair.ids`
`domLCongr_refl` 📖	mathematical	—	`domLCongr` `Equiv.refl` `LinearEquiv.refl` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `module`	—	`LinearEquiv.ext` `RingHomInvPair.ids` `equivMapDomain_refl`
`domLCongr_single` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `domLCongr` `single` `Equiv` `Equiv.instEquivLike`	—	`RingHomInvPair.ids` `equivMapDomain_single`
`domLCongr_symm` 📖	mathematical	—	`LinearEquiv.symm` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `domLCongr` `Equiv.symm`	—	`LinearEquiv.ext` `RingHomInvPair.ids`
`domLCongr_trans` 📖	mathematical	—	`LinearEquiv.trans` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `RingHomInvPair.ids` `domLCongr` `Equiv.trans`	—	`LinearEquiv.ext` `RingHomInvPair.ids` `RingHomCompTriple.ids` `equivMapDomain_trans`
`lcongr_apply_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instFunLike` `LinearEquiv` `instAddCommMonoid` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `lcongr` `Equiv` `Equiv.instEquivLike` `Equiv.symm`	—	—
`lcongr_single` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `lcongr` `single` `Equiv` `Equiv.instEquivLike`	—	`RingHomInvPair.ids` `equivMapDomain_single` `mapRange_single` `LinearEquiv.map_zero`
`lcongr_symm` 📖	mathematical	—	`LinearEquiv.symm` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `module` `lcongr` `Equiv.symm`	—	`LinearEquiv.ext` `ext`
`lcongr_symm_single` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `lcongr` `single` `Equiv` `Equiv.instEquivLike` `Equiv.symm`	—	`LinearEquiv.injective` `LinearEquiv.apply_symm_apply` `lcongr_single` `Equiv.apply_symm_apply`
`lift_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `module` `Semiring.toModule` `LinearMap.instFunLike` `AddEquiv` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearMap.instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `lift` `sum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—
`lift_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `module` `Semiring.toModule` `LinearMap.instAdd` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `lift` `LinearMap.instFunLike` `single` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—
`llift_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `module` `Semiring.toModule` `LinearMap.instFunLike` `LinearEquiv` `RingHomInvPair.ids` `Pi.addCommMonoid` `LinearMap.addCommMonoid` `Pi.Function.module` `LinearMap.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `llift` `AddEquiv` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearMap.instAdd` `AddEquiv.instEquivLike` `lift`	—	`RingHomInvPair.ids`
`llift_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearMap` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `module` `Semiring.toModule` `LinearMap.addCommMonoid` `Pi.addCommMonoid` `LinearMap.module` `Pi.Function.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `llift` `LinearMap.instFunLike` `single` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`RingHomInvPair.ids`
`lsum_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `module` `LinearMap.instFunLike` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Pi.addCommMonoid` `LinearMap.addCommMonoid` `Pi.Function.module` `LinearMap.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `lsum` `sum`	—	`RingHomInvPair.ids`
`lsum_comp_lsingle` 📖	mathematical	—	`LinearMap.comp` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `DFunLike.coe` `LinearEquiv` `RingHomInvPair.ids` `LinearMap` `Pi.addCommMonoid` `LinearMap.addCommMonoid` `Pi.Function.module` `LinearMap.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `lsum` `lsingle`	—	`LinearMap.ext` `RingHomCompTriple.ids` `RingHomInvPair.ids` `sum_single_index` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`lsum_single` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `module` `LinearMap.instFunLike` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Pi.addCommMonoid` `LinearMap.addCommMonoid` `Pi.Function.module` `LinearMap.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `lsum` `single`	—	`sum_single_index` `LinearMap.map_zero`
`lsum_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearMap` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `module` `LinearMap.addCommMonoid` `Pi.addCommMonoid` `LinearMap.module` `Pi.Function.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `lsum` `LinearMap.comp` `RingHomCompTriple.ids` `lsingle`	—	`RingHomInvPair.ids`
`smul_sum` 📖	mathematical	—	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `sum`	—	`Finset.smul_sum`
`sum_smul_index_linearMap'` 📖	mathematical	—	`sum` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp` `SMulZeroClass.toSMul` `instZero` `smulZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	—	`sum_smul_index_semilinearMap'`
`sum_smul_index_semilinearMap'` 📖	mathematical	—	`sum` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp` `SMulZeroClass.toSMul` `instZero` `smulZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`sum_smul_index'` `LinearMap.map_zero` `smul_sum` `MulActionSemiHomClass.map_smulₛₗ` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass`

LinearMap

Definitions

Name	Category	Theorems
`splittingOfFinsuppSurjective` 📖	CompOp	3 math math: `leftInverse_splittingOfFinsuppSurjective`, `splittingOfFinsuppSurjective_injective`, `splittingOfFinsuppSurjective_splits`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_finsupp_sum` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `instFunLike` `Finsupp.sum` `addCommMonoid`	—	—
`finsupp_sum_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `instFunLike` `Finsupp.sum` `addCommMonoid`	—	`sum_apply`
`leftInverse_splittingOfFinsuppSurjective` 📖	mathematical	`Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `LinearMap` `RingHom.id` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `instFunLike`	`splittingOfFinsuppSurjective`	—	`congr_fun` `RingHomCompTriple.ids` `splittingOfFinsuppSurjective_splits`
`splittingOfFinsuppSurjective_injective` 📖	mathematical	`Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `LinearMap` `RingHom.id` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `instFunLike`	`splittingOfFinsuppSurjective`	—	`leftInverse_splittingOfFinsuppSurjective`
`splittingOfFinsuppSurjective_splits` 📖	mathematical	`Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `LinearMap` `RingHom.id` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `instFunLike`	`comp` `RingHomCompTriple.ids` `splittingOfFinsuppSurjective` `id`	—	`Finsupp.lhom_ext'` `RingHomCompTriple.ids` `ext_ring` `Finsupp.ext` `Finsupp.sum_single_index` `zero_smul` `one_smul`

LinearMap.CompatibleSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finsupp_cod` 📖	mathematical	—	`LinearMap.CompatibleSMul` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddCommMonoid` `SMulZeroClass.toSMul` `Finsupp.instZero` `Finsupp.smulZeroClass` `Finsupp.module`	—	`Finsupp.ext` `LinearMap.map_smul_of_tower` `RingHomCompTriple.ids`
`finsupp_dom` 📖	mathematical	—	`LinearMap.CompatibleSMul` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddCommMonoid` `SMulZeroClass.toSMul` `Finsupp.instZero` `Finsupp.smulZeroClass` `Finsupp.module` `DistribSMul.toSMulZeroClass`	—	`Finsupp.sum_single` `map_finsuppSum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Finsupp.smul_sum` `smul_zero` `Finsupp.sum_mapRange_index` `Finsupp.single_zero` `LinearMap.map_smul_of_tower` `RingHomCompTriple.ids`

Submodule

Definitions

Name	Category	Theorems
`mulLeftMap` 📖	CompOp	7 math math: `mulLeftMap_eq_mulRightMap`, `mulLeftMap_apply`, `mulLeftMap_eq_mulRightMap_of_commute`, `mulLeftMap_eq_mulMap_comp`, `mulLeftMap_apply_single`, `LinearDisjoint.linearIndependent_left_of_flat`, `Subalgebra.LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op`
`mulRightMap` 📖	CompOp	7 math math: `mulLeftMap_eq_mulRightMap`, `mulLeftMap_eq_mulRightMap_of_commute`, `LinearDisjoint.linearIndependent_right_of_flat`, `Subalgebra.LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent`, `mulRightMap_eq_mulMap_comp`, `mulRightMap_apply`, `mulRightMap_apply_single`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finsuppSum_mem` 📖	mathematical	`Submodule` `SetLike.instMembership` `setLike` `DFunLike.coe` `Finsupp` `Finsupp.instFunLike`	`Finsupp.sum`	—	`AddSubmonoidClass.finsuppSum_mem` `addSubmonoidClass`
`mulLeftMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `setLike` `zero` `Finsupp.instAddCommMonoid` `addCommMonoid` `Finsupp.module` `module` `LinearMap.instFunLike` `mulLeftMap` `Finsupp.sum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`mulLeftMap_apply_single` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `setLike` `zero` `Finsupp.instAddCommMonoid` `addCommMonoid` `Finsupp.module` `module` `LinearMap.instFunLike` `mulLeftMap` `Finsupp.single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`Finsupp.sum_single_index` `MulZeroClass.mul_zero`
`mulLeftMap_eq_mulRightMap` 📖	mathematical	—	`mulLeftMap` `CommSemiring.toSemiring` `mulRightMap`	—	`mulLeftMap_eq_mulRightMap_of_commute` `mul_comm`
`mulLeftMap_eq_mulRightMap_of_commute` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `SetLike.instMembership` `setLike`	`mulLeftMap` `mulRightMap`	—	`Finsupp.lhom_ext'` `LinearMap.ext` `RingHomCompTriple.ids` `mulLeftMap_apply_single` `Commute.eq` `mulRightMap_apply_single`
`mulRightMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `setLike` `zero` `Finsupp.instAddCommMonoid` `addCommMonoid` `Finsupp.module` `module` `LinearMap.instFunLike` `mulRightMap` `Finsupp.sum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`mulRightMap_apply_single` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `setLike` `zero` `Finsupp.instAddCommMonoid` `addCommMonoid` `Finsupp.module` `module` `LinearMap.instFunLike` `mulRightMap` `Finsupp.single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`Finsupp.sum_single_index` `smul_zero`

---

← Back to Index