Basic

📁 Source: Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean

Statistics

Metric	Count
Definitions `SkewMonoidAlgebra`, `single`, `basisSingleOne`, `coeff`, `comapDistribMulActionSelf`, `comapMulAction`, `comapSMul`, `instAdd`, `instAddCommGroup`, `instAddCommMonoid`, `instAddGroup`, `instAddGroupWithOne`, `instAddMonoid`, `instAddMonoidWithOne`, `instAlgebraOfSMulCommClass`, `instCommSemiring`, `instDecidableEq`, `instDistribMulAction`, `instDistribSMul`, `instInhabited`, `instModule`, `instMul`, `instNeg`, `instNonAssocRing`, `instNonAssocSemiring`, `instNonUnitalNonAssocRing`, `instNonUnitalNonAssocSemiring`, `instNonUnitalRing`, `instNonUnitalSemiring`, `instOne`, `instRing`, `instSMulZeroClass`, `instSemiring`, `instUniqueOfSubsingleton`, `instZero`, `liftNC`, `liftNCRingHom`, `lsingle`, `mapDomain`, `mapDomainRingHom`, `of`, `single`, `singleAddHom`, `singleOneRingHom`, `sum`, `support`, `toFinsupp`, `toFinsuppAddEquiv`, `toFinsuppLinearEquiv`	49
Theorems `skewMonoidAlgebra`, `skewMonoidAlgebra_iff`, `single_toFun`, `addHom_ext`, `addHom_ext'`, `addHom_ext'_iff`, `addHom_ext_iff`, `algHom_ext`, `algHom_ext'`, `algHom_ext'_iff`, `coe_algebraMap`, `coeff_add`, `coeff_inj`, `coeff_injective`, `coeff_mul`, `coeff_mul_antidiagonal_finsum`, `coeff_mul_antidiagonal_of_finset`, `coeff_mul_left`, `coeff_mul_right`, `coeff_mul_single`, `coeff_mul_single_aux`, `coeff_mul_single_of_not_exists_mul`, `coeff_mul_single_one`, `coeff_ofFinsupp`, `coeff_one`, `coeff_one_one`, `coeff_single`, `coeff_single_apply`, `coeff_single_mul`, `coeff_single_mul_aux`, `coeff_single_mul_of_not_exists_mul`, `coeff_single_one_mul`, `coeff_smul`, `coeff_sum`, `coeff_zero`, `comapSMul_def`, `comapSMul_single`, `distribMulActionHom_ext`, `distribMulActionHom_ext'`, `distribMulActionHom_ext'_iff`, `eq_liftNC`, `eta`, `ext`, `ext_iff`, `induction_on`, `induction_on'`, `instFaithfulSMul`, `instFree`, `instIsCentralScalar`, `instIsScalarTower`, `instNontrivialOfNonempty`, `instSMulCommClass`, `intCast_def`, `isScalarTower_self`, `lhom_ext`, `lhom_ext'`, `lhom_ext'_iff`, `liftNC_mul`, `liftNC_one`, `liftNC_single`, `liftNC_smul`, `mapDomain_apply`, `mapDomain_comp`, `mapDomain_id`, `mapDomain_mul`, `mapDomain_one`, `mapDomain_single`, `mapDomain_smul`, `map_sum`, `mem_support_iff`, `mul_def`, `mul_sum`, `natCast_def`, `nonUnitalAlgHom_ext`, `nonUnitalAlgHom_ext'`, `nonUnitalAlgHom_ext'_iff`, `notMem_support_iff`, `ofFinsupp_add`, `ofFinsupp_eq_one`, `ofFinsupp_eq_zero`, `ofFinsupp_inj`, `ofFinsupp_injective`, `ofFinsupp_neg`, `ofFinsupp_one`, `ofFinsupp_single`, `ofFinsupp_smul`, `ofFinsupp_sub`, `ofFinsupp_sum`, `ofFinsupp_zero`, `of_apply`, `of_injective`, `one_def`, `ringHom_ext`, `ringHom_ext'`, `ringHom_ext'_iff`, `singleAddHom_apply`, `single_add`, `single_algebraMap_eq_algebraMap_mul_of`, `single_eq_algebraMap_mul_of`, `single_eq_zero`, `single_injective`, `single_left_inj`, `single_mul_single`, `single_nat`, `single_neg`, `single_one_one`, `single_zero`, `single_zero_right`, `smul_of`, `smul_single`, `smul_sum`, `sum_add`, `sum_add_index`, `sum_add_index'`, `sum_congr`, `sum_def`, `sum_def'`, `sum_ite_eq'`, `sum_mapDomain_index`, `sum_mul`, `sum_single`, `sum_single_index`, `sum_smul_index`, `sum_smul_index'`, `sum_sum_index`, `sum_zero`, `sum_zero_index`, `support_add`, `support_eq_empty`, `support_ofFinsupp`, `support_toFinsupp`, `support_zero`, `toFinsuppAddEquiv_apply`, `toFinsuppAddEquiv_symm_apply`, `toFinsupp_add`, `toFinsupp_apply`, `toFinsupp_eq_single_one_one_iff`, `toFinsupp_eq_zero`, `toFinsupp_inj`, `toFinsupp_injective`, `toFinsupp_mapDomain`, `toFinsupp_neg`, `toFinsupp_one`, `toFinsupp_single`, `toFinsupp_smul`, `toFinsupp_sub`, `toFinsupp_sum'`, `toFinsupp_zero`	148
Total	197

IsSMulRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`skewMonoidAlgebra` 📖	mathematical	`IsSMulRegular` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	`SkewMonoidAlgebra` `SkewMonoidAlgebra.instZero` `SkewMonoidAlgebra.instSMulZeroClass`	—	`finsupp`
`skewMonoidAlgebra_iff` 📖	mathematical	—	`IsSMulRegular` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `SkewMonoidAlgebra` `SkewMonoidAlgebra.instZero` `SkewMonoidAlgebra.instSMulZeroClass`	—	`skewMonoidAlgebra` `SkewMonoidAlgebra.single_injective` `SkewMonoidAlgebra.smul_single`

SkewMonoidAlgebra

Definitions

Name	Category	Theorems
`basisSingleOne` 📖	CompOp	—
`coeff` 📖	CompOp	41 math math: `toFinsupp_apply`, `coeff_update_ne`, `coeff_single_one_mul`, `sum_def'`, `coeff_single_mul_of_not_exists_mul`, `coeff_erase_same`, `domCongrAlg_apply`, `coeff_erase_ne`, `support_sum`, `update_self`, `coeff_sum`, `coeff_inj`, `coeff_mul_single_of_not_exists_mul`, `coeff_mul_right`, `coeff_equivMapDomain`, `coeff_one_one`, `coeff_zero`, `sum_ite_eq'`, `coeff_mul`, `coeff_mul_antidiagonal_finsum`, `coeff_mul_single`, `coeff_one`, `coeff_mul_single_one`, `coeff_update_apply`, `coeff_ofFinsupp`, `notMem_support_iff`, `coeff_mul_antidiagonal_of_finset`, `coeff_update_same`, `coeff_mul_left`, `coeff_mul_single_aux`, `coeff_injective`, `ext_iff`, `coeff_smul`, `single_add_erase`, `coeff_single_mul_aux`, `coeff_single`, `coeff_single_apply`, `coeff_update`, `coeff_single_mul`, `coeff_add`, `coeff_erase_apply`
`comapDistribMulActionSelf` 📖	CompOp	—
`comapMulAction` 📖	CompOp	—
`comapSMul` 📖	CompOp	2 math math: `comapSMul_def`, `comapSMul_single`
`instAdd` 📖	CompOp	12 math math: `sum_add_index`, `sum_add_index'`, `toFinsuppAddEquiv_apply`, `update_eq_erase_add_single`, `toFinsuppAddEquiv_symm_apply`, `support_add`, `single_add`, `ofFinsupp_add`, `toFinsupp_add`, `domCongr_apply`, `single_add_erase`, `coeff_add`
`instAddCommGroup` 📖	CompOp	—
`instAddCommMonoid` 📖	CompOp	12 math math: `ofFinsupp_sum`, `support_sum`, `coeff_sum`, `sum_single`, `instFree`, `mapDomainAlgHom_apply`, `lhom_ext'_iff`, `sum_sum_index`, `mem_span_support`, `mapDomain_apply`, `toFinsupp_sum'`, `mul_def`
`instAddGroup` 📖	CompOp	2 math math: `toFinsupp_sub`, `ofFinsupp_sub`
`instAddGroupWithOne` 📖	CompOp	1 math math: `intCast_def`
`instAddMonoid` 📖	CompOp	31 math math: `mapDomain_smul`, `erase_apply_toFinsupp`, `coeff_erase_same`, `mapDomain_one`, `coeff_erase_ne`, `mapDomain_mul`, `mapDomain_single`, `comapSMul_def`, `addHom_ext_iff`, `liftNC_one`, `update_eq_erase_add_single`, `mapDomain_id`, `addHom_ext'_iff`, `liftNC_mul`, `sum_mapDomain_index`, `toFinsupp_mapDomain`, `update_zero_eq_erase`, `isScalarTower_self`, `liftNC_single`, `erase_single`, `distribMulActionHom_ext'_iff`, `single_add_erase`, `lift_def`, `DistribMulActionHom.single_toFun`, `equivMapDomain_eq_mapDomain`, `mapDomain_apply`, `singleAddHom_apply`, `liftNC_smul`, `coeff_erase_apply`, `support_erase`, `mapDomain_comp`
`instAddMonoidWithOne` 📖	CompOp	2 math math: `natCast_def`, `single_nat`
`instAlgebraOfSMulCommClass` 📖	CompOp	19 math math: `domCongr_support`, `algHom_ext'_iff`, `lift_apply'`, `single_algebraMap_eq_algebraMap_mul_of`, `domCongrAlg_apply`, `lift_of`, `lift_single`, `lift_apply`, `lift_unique`, `domCongrAlg_toAlgHom`, `domCongr_refl`, `coe_algebraMap`, `lift_unique'`, `mapDomainAlgHom_apply`, `single_eq_algebraMap_mul_of`, `domCongr_single`, `lift_def`, `domCongr_symm`, `lift_symm_apply`
`instCommSemiring` 📖	CompOp	—
`instDecidableEq` 📖	CompOp	—
`instDistribMulAction` 📖	CompOp	3 math math: `nonUnitalAlgHom_ext'_iff`, `distribMulActionHom_ext'_iff`, `DistribMulActionHom.single_toFun`
`instDistribSMul` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instModule` 📖	CompOp	3 math math: `instFree`, `lhom_ext'_iff`, `mem_span_support`
`instMul` 📖	CompOp	26 math math: `coeff_single_one_mul`, `support_single_mul`, `coeff_single_mul_of_not_exists_mul`, `single_algebraMap_eq_algebraMap_mul_of`, `support_mul_single`, `mapDomain_mul`, `coeff_mul_single_of_not_exists_mul`, `coeff_mul_right`, `support_mul_single_eq_image`, `single_mul_single`, `support_single_mul_eq_image`, `coeff_mul`, `coeff_mul_antidiagonal_finsum`, `support_mul_single_subset`, `coeff_mul_single`, `support_mul`, `liftNC_mul`, `coeff_mul_single_one`, `support_single_mul_subset`, `coeff_mul_antidiagonal_of_finset`, `single_eq_algebraMap_mul_of`, `coeff_mul_left`, `coeff_mul_single_aux`, `coeff_single_mul_aux`, `coeff_single_mul`, `mul_def`
`instNeg` 📖	CompOp	4 math math: `single_neg`, `toFinsupp_neg`, `ofFinsupp_neg`, `support_neg`
`instNonAssocRing` 📖	CompOp	—
`instNonAssocSemiring` 📖	CompOp	11 math math: `algHom_ext'_iff`, `single_algebraMap_eq_algebraMap_mul_of`, `smul_of`, `lift_of`, `nonUnitalAlgHom_ext'_iff`, `of_apply`, `lift_unique'`, `of_injective`, `single_eq_algebraMap_mul_of`, `ringHom_ext'_iff`, `mem_span_support`
`instNonUnitalNonAssocRing` 📖	CompOp	—
`instNonUnitalNonAssocSemiring` 📖	CompOp	2 math math: `nonUnitalAlgHom_ext'_iff`, `isScalarTower_self`
`instNonUnitalRing` 📖	CompOp	—
`instNonUnitalSemiring` 📖	CompOp	—
`instOne` 📖	CompOp	12 math math: `mapDomain_one`, `toFinsupp_eq_single_one_one_iff`, `support_one`, `support_one_subset`, `one_def`, `coeff_one_one`, `liftNC_one`, `toFinsupp_one`, `coeff_one`, `single_one_one`, `ofFinsupp_eq_one`, `ofFinsupp_one`
`instRing` 📖	CompOp	—
`instSMulZeroClass` 📖	CompOp	16 math math: `mapDomain_smul`, `IsSMulRegular.skewMonoidAlgebra`, `ofFinsupp_smul`, `toFinsupp_smul`, `smul_of`, `instFaithfulSMul`, `sum_smul_index'`, `instIsScalarTower`, `smul_single`, `sum_smul_index`, `isScalarTower_self`, `instSMulCommClass`, `IsSMulRegular.skewMonoidAlgebra_iff`, `instIsCentralScalar`, `coeff_smul`, `liftNC_smul`
`instSemiring` 📖	CompOp	19 math math: `domCongr_support`, `algHom_ext'_iff`, `lift_apply'`, `single_algebraMap_eq_algebraMap_mul_of`, `domCongrAlg_apply`, `lift_of`, `lift_single`, `lift_apply`, `lift_unique`, `domCongrAlg_toAlgHom`, `domCongr_refl`, `coe_algebraMap`, `lift_unique'`, `mapDomainAlgHom_apply`, `single_eq_algebraMap_mul_of`, `domCongr_single`, `lift_def`, `domCongr_symm`, `lift_symm_apply`
`instUniqueOfSubsingleton` 📖	CompOp	—
`instZero` 📖	CompOp	29 math math: `mapDomain_smul`, `ofFinsupp_eq_zero`, `IsSMulRegular.skewMonoidAlgebra`, `ofFinsupp_zero`, `ofFinsupp_smul`, `toFinsupp_smul`, `smul_of`, `single_eq_zero`, `support_eq_empty`, `instFaithfulSMul`, `sum_smul_index'`, `single_zero`, `instIsScalarTower`, `coeff_zero`, `smul_single`, `toFinsupp_zero`, `zero_update`, `single_zero_right`, `sum_smul_index`, `support_zero`, `sum_zero_index`, `isScalarTower_self`, `erase_single`, `instSMulCommClass`, `IsSMulRegular.skewMonoidAlgebra_iff`, `instIsCentralScalar`, `toFinsupp_eq_zero`, `coeff_smul`, `liftNC_smul`
`liftNC` 📖	CompOp	6 math math: `liftNC_one`, `liftNC_mul`, `liftNC_single`, `eq_liftNC`, `lift_def`, `liftNC_smul`
`liftNCRingHom` 📖	CompOp	—
`lsingle` 📖	CompOp	1 math math: `lhom_ext'_iff`
`mapDomain` 📖	CompOp	11 math math: `mapDomain_smul`, `mapDomain_one`, `mapDomain_mul`, `mapDomain_single`, `comapSMul_def`, `mapDomain_id`, `sum_mapDomain_index`, `toFinsupp_mapDomain`, `equivMapDomain_eq_mapDomain`, `mapDomain_apply`, `mapDomain_comp`
`mapDomainRingHom` 📖	CompOp	—
`of` 📖	CompOp	11 math math: `algHom_ext'_iff`, `single_algebraMap_eq_algebraMap_mul_of`, `smul_of`, `lift_of`, `nonUnitalAlgHom_ext'_iff`, `of_apply`, `lift_unique'`, `of_injective`, `single_eq_algebraMap_mul_of`, `ringHom_ext'_iff`, `mem_span_support`
`single` 📖	CompOp	59 math math: `single_neg`, `single_injective`, `coeff_single_one_mul`, `support_single_mul`, `coeff_single_mul_of_not_exists_mul`, `single_algebraMap_eq_algebraMap_mul_of`, `smul_of`, `support_mul_single`, `toFinsupp_single`, `mapDomain_single`, `single_eq_zero`, `SkewPolynomial.monomial_def`, `one_def`, `addHom_ext_iff`, `lift_single`, `coeff_mul_single_of_not_exists_mul`, `of_apply`, `sum_single`, `lift_unique`, `support_mul_single_eq_image`, `single_left_inj`, `single_zero`, `single_mul_single`, `support_single_mul_eq_image`, `comapSMul_single`, `coe_algebraMap`, `update_eq_erase_add_single`, `smul_single`, `zero_update`, `single_zero_right`, `single_add`, `support_mul_single_subset`, `coeff_mul_single`, `mapDomainAlgHom_apply`, `single_one_one`, `coeff_mul_single_one`, `support_single_subset`, `natCast_def`, `liftNC_single`, `intCast_def`, `erase_single`, `support_single_mul_subset`, `single_nat`, `single_eq_algebraMap_mul_of`, `ofFinsupp_single`, `coeff_mul_single_aux`, `domCongr_single`, `single_add_erase`, `coeff_single_mul_aux`, `coeff_single`, `coeff_single_apply`, `equivMapDomain_single`, `mapDomain_apply`, `singleAddHom_apply`, `coeff_single_mul`, `sum_single_index`, `mul_def`, `lift_symm_apply`, `support_single_ne_zero`
`singleAddHom` 📖	CompOp	3 math math: `addHom_ext'_iff`, `DistribMulActionHom.single_toFun`, `singleAddHom_apply`
`singleOneRingHom` 📖	CompOp	1 math math: `ringHom_ext'_iff`
`sum` 📖	CompOp	32 math math: `sum_add_index`, `sum_def'`, `lift_apply'`, `sum_add_index'`, `ofFinsupp_sum`, `support_sum`, `coeff_sum`, `lift_apply`, `sum_def`, `coeff_mul_right`, `sum_single`, `lift_unique`, `sum_smul_index'`, `sum_ite_eq'`, `sum_mul`, `coeff_mul`, `map_sum`, `sum_smul_index`, `mapDomainAlgHom_apply`, `sum_mapDomain_index`, `smul_sum`, `mul_sum`, `sum_zero_index`, `sum_sum_index`, `sum_congr`, `coeff_mul_left`, `sum_add`, `sum_zero`, `mapDomain_apply`, `toFinsupp_sum'`, `sum_single_index`, `mul_def`
`support` 📖	CompOp	26 math math: `domCongr_support`, `sum_def'`, `support_single_mul`, `support_mul_single`, `support_one`, `support_one_subset`, `support_sum`, `support_eq_empty`, `support_toFinsupp`, `support_mul_single_eq_image`, `support_single_mul_eq_image`, `sum_ite_eq'`, `mem_support_iff`, `support_add`, `support_zero`, `support_mul_single_subset`, `support_mul`, `support_single_subset`, `support_neg`, `support_ofFinsupp`, `notMem_support_iff`, `support_single_mul_subset`, `support_update`, `mem_span_support`, `support_erase`, `support_single_ne_zero`
`toFinsupp` 📖	CompOp	21 math math: `toFinsupp_apply`, `erase_apply_toFinsupp`, `toFinsupp_smul`, `eta`, `toFinsupp_eq_single_one_one_iff`, `toFinsupp_single`, `support_toFinsupp`, `sum_def`, `toFinsupp_sub`, `toFinsuppAddEquiv_apply`, `toFinsupp_injective`, `toFinsupp_neg`, `toFinsupp_equivMapDomain`, `toFinsupp_zero`, `toFinsupp_one`, `toFinsupp_add`, `update_toFinsupp`, `toFinsupp_mapDomain`, `toFinsupp_eq_zero`, `toFinsupp_inj`, `toFinsupp_sum'`
`toFinsuppAddEquiv` 📖	CompOp	2 math math: `toFinsuppAddEquiv_apply`, `toFinsuppAddEquiv_symm_apply`
`toFinsuppLinearEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addHom_ext` 📖	—	`DFunLike.coe` `AddMonoidHom` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddMonoid` `AddMonoidHom.instFunLike` `single`	—	—	`AddMonoidHom.ext` `induction_on` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `map_add` `AddMonoidHomClass.toAddHomClass`
`addHom_ext'` 📖	—	`AddMonoidHom.comp` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddMonoid` `singleAddHom`	—	—	`addHom_ext` `DFunLike.congr_fun`
`addHom_ext'_iff` 📖	mathematical	—	`AddMonoidHom.comp` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddMonoid` `singleAddHom`	—	`addHom_ext'`
`addHom_ext_iff` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddMonoid` `AddMonoidHom.instFunLike` `single`	—	`addHom_ext`
`algHom_ext` 📖	—	`DFunLike.coe` `AlgHom` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSemiring` `instAlgebraOfSMulCommClass` `Algebra.id` `AlgHom.funLike` `single` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—	`AlgHom.toLinearMap_injective` `lhom_ext'` `LinearMap.ext_ring` `RingHomCompTriple.ids`
`algHom_ext'` 📖	—	`MonoidHom.comp` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `instNonAssocSemiring` `MonoidHomClass.toMonoidHom` `AlgHom` `instSemiring` `instAlgebraOfSMulCommClass` `Algebra.id` `AlgHom.funLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `of`	—	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `algHom_ext` `DFunLike.congr_fun`
`algHom_ext'_iff` 📖	mathematical	—	`MonoidHom.comp` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `instNonAssocSemiring` `MonoidHomClass.toMonoidHom` `AlgHom` `instSemiring` `instAlgebraOfSMulCommClass` `Algebra.id` `AlgHom.funLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `of`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `algHom_ext'`
`coe_algebraMap` 📖	mathematical	—	`DFunLike.coe` `RingHom` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebraOfSMulCommClass` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `single` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—
`coeff_add` 📖	mathematical	—	`coeff` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	—	`Finsupp.add_apply`
`coeff_inj` 📖	mathematical	—	`coeff`	—	`coeff_injective`
`coeff_injective` 📖	mathematical	—	`SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `coeff`	—	—
`coeff_mul` 📖	mathematical	—	`coeff` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `sum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_def` `coeff_sum` `coeff_single_apply`
`coeff_mul_antidiagonal_finsum` 📖	mathematical	—	`coeff` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `finsum` `Set` `Set.instMembership` `setOf` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`Set.Finite.inter_of_right` `Set.Finite.subset` `Finset.finite_toSet` `Finset.coe_product` `MulZeroClass.zero_mul` `smul_zero` `MulZeroClass.mul_zero` `finsum_mem_inter_support` `finsum_mem_eq_finite_toFinset_sum` `coeff_mul` `Finset.sum_product` `Finset.sum_filter` `Finset.sum_congr_of_eq_on_inter` `Finset.filter.congr_simp` `Finset.sum_subset` `Finset.filter_subset`
`coeff_mul_antidiagonal_of_finset` 📖	mathematical	`Finset` `Finset.instMembership` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`coeff` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `Finset.sum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`coeff_mul` `Finset.sum_product` `Finset.sum_filter` `Finset.sum_congr` `Finset.ext` `Finset.filter.congr_simp` `Finset.sum_subset` `Finset.filter_subset` `MulZeroClass.zero_mul` `smul_zero` `MulZeroClass.mul_zero`
`coeff_mul_left` 📖	mathematical	—	`coeff` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `sum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`coeff_sum` `sum_mul` `sum_single` `coeff_single_mul`
`coeff_mul_right` 📖	mathematical	—	`coeff` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `sum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`coeff_sum` `mul_sum` `sum_single` `coeff_mul_single`
`coeff_mul_single` 📖	mathematical	—	`coeff` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`coeff_mul_single_aux` `eq_mul_inv_iff_mul_eq`
`coeff_mul_single_aux` 📖	mathematical	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`coeff` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `instMul` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`sum_single_index` `smul_zero` `MulZeroClass.mul_zero` `coeff_mul` `sum_ite_eq'` `Finset.sum_ite_eq'` `MulZeroClass.zero_mul`
`coeff_mul_single_of_not_exists_mul` 📖	mathematical	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`coeff` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `instMul` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `single`	—	`coeff_mul` `sum_single_index` `smul_zero` `MulZeroClass.mul_zero` `Finset.sum_eq_zero`
`coeff_mul_single_one` 📖	mathematical	—	`coeff` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `single` `MulOne.toOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`coeff_mul_single_aux` `mul_one`
`coeff_ofFinsupp` 📖	mathematical	—	`coeff` `ofFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DFunLike.coe` `Finsupp` `Finsupp.instFunLike`	—	—
`coeff_one` 📖	mathematical	—	`coeff` `AddMonoidWithOne.toAddMonoid` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instOne` `AddMonoidWithOne.toOne`	—	`coeff_single_apply`
`coeff_one_one` 📖	mathematical	—	`coeff` `AddMonoidWithOne.toAddMonoid` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instOne` `AddMonoidWithOne.toOne`	—	`Finsupp.single_eq_same`
`coeff_single` 📖	mathematical	—	`coeff` `single` `Pi.single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`Finsupp.single_eq_pi_single`
`coeff_single_apply` 📖	mathematical	—	`coeff` `single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`Finsupp.single_apply`
`coeff_single_mul` 📖	mathematical	—	`coeff` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`coeff_single_mul_aux` `eq_inv_mul_iff_mul_eq`
`coeff_single_mul_aux` 📖	mathematical	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`coeff` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instMul` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`MulZeroClass.zero_mul` `sum_zero` `coeff_mul` `sum_single_index` `sum_ite_eq'` `Finset.sum_ite_eq'` `smul_zero` `MulZeroClass.mul_zero`
`coeff_single_mul_of_not_exists_mul` 📖	mathematical	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`coeff` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instMul` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `single`	—	`coeff_mul` `sum_single_index` `MulZeroClass.zero_mul` `sum_zero` `Finset.sum_eq_zero`
`coeff_single_one_mul` 📖	mathematical	—	`coeff` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `single` `MulOne.toOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`coeff_single_mul_aux` `one_mul` `one_smul`
`coeff_smul` 📖	mathematical	—	`coeff` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SMulZeroClass.toSMul` `instZero` `instSMulZeroClass`	—	—
`coeff_sum` 📖	mathematical	—	`coeff` `AddCommMonoid.toAddMonoid` `sum` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddCommMonoid`	—	`toFinsupp_sum'` `Finsupp.sum_apply`
`coeff_zero` 📖	mathematical	—	`coeff` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instZero`	—	—
`comapSMul_def` 📖	mathematical	—	`SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `comapSMul` `DFunLike.coe` `AddMonoidHom` `instAddMonoid` `AddMonoidHom.instFunLike` `mapDomain` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	—
`comapSMul_single` 📖	mathematical	—	`SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `comapSMul` `single` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`mapDomain_single`
`distribMulActionHom_ext` 📖	—	`DFunLike.coe` `DistribMulActionHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddMonoid` `instDistribMulAction` `DistribMulActionHom.instFunLike` `single`	—	—	`DistribMulActionHom.toAddMonoidHom_injective` `addHom_ext` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `DistribMulActionHom.instDistribMulActionSemiHomClassCoeMonoidHom`
`distribMulActionHom_ext'` 📖	—	`DistribMulActionHom.comp` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `AddCommMonoid.toAddMonoid` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddMonoid` `instDistribMulAction` `DistribMulActionHom.single` `MonoidHom.CompTriple.instId_comp` `MonoidHom.CompTriple.instIsId`	—	—	`MonoidHom.CompTriple.instId_comp` `MonoidHom.CompTriple.instIsId` `distribMulActionHom_ext` `DistribMulActionHom.congr_fun`
`distribMulActionHom_ext'_iff` 📖	mathematical	—	`DistribMulActionHom.comp` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `AddCommMonoid.toAddMonoid` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddMonoid` `instDistribMulAction` `DistribMulActionHom.single` `MonoidHom.CompTriple.instId_comp` `MonoidHom.CompTriple.instIsId`	—	`MonoidHom.CompTriple.instId_comp` `MonoidHom.CompTriple.instIsId` `distribMulActionHom_ext'`
`eq_liftNC` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoidHom.instFunLike` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`liftNC`	—	`addHom_ext` `liftNC_single`
`eta` 📖	mathematical	—	`ofFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `toFinsupp`	—	—
`ext` 📖	—	`coeff`	—	—	`ext_iff`
`ext_iff` 📖	mathematical	—	`coeff`	—	`DFunLike.ext_iff`
`induction_on` 📖	—	`SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instZero` `single` `instAdd`	—	—	`sum_single` `sum_def'` `Finset.sum_induction`
`induction_on'` 📖	—	`single` `AddCommMonoid.toAddMonoid` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAdd`	—	—	`induction_on` `single_zero`
`instFaithfulSMul` 📖	mathematical	—	`FaithfulSMul` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SMulZeroClass.toSMul` `instZero` `instSMulZeroClass`	—	`FaithfulSMul.eq_of_smul_eq_smul` `Finsupp.faithfulSMul` `ofFinsupp_smul`
`instFree` 📖	mathematical	—	`Module.Free` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instModule` `Semiring.toModule`	—	`Module.Free.of_basis`
`instIsCentralScalar` 📖	mathematical	—	`IsCentralScalar` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SMulZeroClass.toSMul` `instZero` `instSMulZeroClass` `MulOpposite`	—	`IsCentralScalar.op_smul_eq_smul` `Finsupp.isCentralScalar`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SMulZeroClass.toSMul` `instZero` `instSMulZeroClass`	—	`smul_assoc` `Finsupp.isScalarTower`
`instNontrivialOfNonempty` 📖	mathematical	—	`Nontrivial` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`Function.Injective.nontrivial` `Finsupp.instNontrivial` `ofFinsupp_injective`
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SMulZeroClass.toSMul` `instZero` `instSMulZeroClass`	—	`SMulCommClass.smul_comm` `Finsupp.smulCommClass`
`intCast_def` 📖	mathematical	—	`SkewMonoidAlgebra` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddGroupWithOne.toAddGroup` `AddGroupWithOne.toIntCast` `instAddGroupWithOne` `single` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne`	—	`Int.cast_natCast` `single_nat` `Int.cast_negSucc` `Nat.cast_add` `Nat.cast_one` `neg_add_rev` `single_add` `single_neg`
`isScalarTower_self` 📖	mathematical	—	`IsScalarTower` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SMulZeroClass.toSMul` `instZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instSMulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `instDistribSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `instAddMonoid` `instNonUnitalNonAssocSemiring` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction`	—	`sum_smul_index'` `MulZeroClass.zero_mul` `single_zero` `sum_zero` `smul_mul_assoc`
`lhom_ext` 📖	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `instModule` `LinearMap.instFunLike` `single`	—	—	`LinearMap.toAddMonoidHom_injective` `addHom_ext`
`lhom_ext'` 📖	—	`LinearMap.comp` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `lsingle`	—	—	`RingHomCompTriple.ids` `lhom_ext` `LinearMap.congr_fun`
`lhom_ext'_iff` 📖	mathematical	—	`LinearMap.comp` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `instModule` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `lsingle`	—	`RingHomCompTriple.ids` `lhom_ext'`
`liftNC_mul` 📖	mathematical	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `coeff` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid`	`AddMonoidHom` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddMonoid` `AddMonoidHom.instFunLike` `liftNC` `AddMonoidHomClass.toAddMonoidHom` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instMul`	—	`RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `sum_single` `map_sum` `AddMonoidHom.instAddMonoidHomClass` `liftNC_single` `sum_mul` `mul_sum` `sum_congr` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `mul_assoc`
`liftNC_one` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instAddMonoid` `Semiring.toNonAssocSemiring` `AddMonoidHom.instFunLike` `liftNC` `AddMonoidHomClass.toAddMonoidHom` `RingHom` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `RingHom.instFunLike` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `instOne` `AddMonoidWithOne.toOne`	—	`RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `liftNC_single` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `mul_one`
`liftNC_single` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoidHom.instFunLike` `liftNC` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`Finsupp.liftAddHom_apply_single`
`liftNC_smul` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instAddMonoid` `AddMonoidHom.instFunLike` `liftNC` `AddMonoidHomClass.toAddMonoidHom` `RingHom` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `RingHom.instFunLike` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MonoidHom.instFunLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `SMulZeroClass.toSMul` `instZero` `instSMulZeroClass` `DistribSMul.toSMulZeroClass` `instDistribSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `addHom_ext'` `AddMonoidHom.ext` `smul_single` `liftNC_single` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `mul_assoc`
`mapDomain_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddMonoid` `AddMonoidHom.instFunLike` `mapDomain` `sum` `instAddCommMonoid` `single`	—	—
`mapDomain_comp` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddMonoid` `AddMonoidHom.instFunLike` `mapDomain`	—	`sum_sum_index` `single_zero` `single_add` `sum_congr` `sum_single_index`
`mapDomain_id` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddMonoid` `AddMonoidHom.instFunLike` `mapDomain`	—	`sum_single`
`mapDomain_mul` 📖	mathematical	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `DFunLike.coe`	`AddMonoidHom` `SkewMonoidAlgebra` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instAddMonoid` `AddMonoidHom.instFunLike` `mapDomain` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`mul_def` `map_sum` `AddMonoidHom.instAddMonoidHomClass` `mapDomain_single` `map_mul` `sum_mapDomain_index` `MulZeroClass.zero_mul` `single_zero` `sum_zero` `add_mul` `Distrib.rightDistribClass` `single_add` `sum_add` `ext` `smul_zero` `MulZeroClass.mul_zero` `smul_add` `mul_add` `Distrib.leftDistribClass`
`mapDomain_one` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instAddMonoid` `AddMonoidHom.instFunLike` `mapDomain` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instOne` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`mapDomain_single` `map_one` `MonoidHomClass.toOneHomClass`
`mapDomain_single` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddMonoid` `AddMonoidHom.instFunLike` `mapDomain` `single`	—	`sum_single_index` `single_zero`
`mapDomain_smul` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddMonoid` `AddMonoidHom.instFunLike` `mapDomain` `SMulZeroClass.toSMul` `instZero` `instSMulZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	`toFinsupp_smul` `toFinsupp_mapDomain` `Finsupp.mapDomain_smul`
`map_sum` 📖	mathematical	—	`DFunLike.coe` `sum`	—	`map_sum`
`mem_support_iff` 📖	mathematical	—	`Finset` `Finset.instMembership` `support`	—	`support_ofFinsupp`
`mul_def` 📖	mathematical	—	`SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instMul` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`mul_sum` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`Finset.mul_sum` `Finset.sum_congr`
`natCast_def` 📖	mathematical	—	`SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddMonoidWithOne.toNatCast` `instAddMonoidWithOne` `single`	—	`Nat.cast_zero` `single_zero` `Nat.cast_add` `Nat.cast_one` `single_add`
`nonUnitalAlgHom_ext` 📖	—	`DFunLike.coe` `NonUnitalAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instNonUnitalNonAssocSemiring` `MulOne.toMul` `Monoid.toMulOneClass` `DistribMulAction.toDistribSMul` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `MulSemiringAction.toDistribMulAction` `instDistribMulAction` `Module.toDistribMulAction` `Semiring.toModule` `NonUnitalAlgHom.instFunLike_1` `single` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—	`NonUnitalAlgHom.to_distribMulActionHom_injective` `distribMulActionHom_ext'` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `NonUnitalAlgHom.instNonUnitalAlgSemiHomClass` `DistribMulActionHom.ext_ring` `MonoidHom.CompTriple.instId_comp` `MonoidHom.CompTriple.instIsId`
`nonUnitalAlgHom_ext'` 📖	—	`MulHom.comp` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `instNonUnitalNonAssocSemiring` `DistribMulAction.toDistribSMul` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `MulSemiringAction.toDistribMulAction` `NonUnitalAlgHom.toMulHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MonoidHom.id` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `instDistribMulAction` `Module.toDistribMulAction` `Semiring.toModule` `MonoidHom.toMulHom` `instNonAssocSemiring` `of`	—	—	`nonUnitalAlgHom_ext` `DFunLike.congr_fun`
`nonUnitalAlgHom_ext'_iff` 📖	mathematical	—	`MulHom.comp` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `instNonUnitalNonAssocSemiring` `DistribMulAction.toDistribSMul` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `MulSemiringAction.toDistribMulAction` `NonUnitalAlgHom.toMulHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MonoidHom.id` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `instDistribMulAction` `Module.toDistribMulAction` `Semiring.toModule` `MonoidHom.toMulHom` `instNonAssocSemiring` `of`	—	`nonUnitalAlgHom_ext'`
`notMem_support_iff` 📖	mathematical	—	`Finset` `Finset.instMembership` `support` `coeff` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	—
`ofFinsupp_add` 📖	mathematical	—	`ofFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Finsupp` `Finsupp.instAdd` `SkewMonoidAlgebra` `instAdd`	—	—
`ofFinsupp_eq_one` 📖	mathematical	—	`ofFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `SkewMonoidAlgebra` `instOne` `Finsupp.single` `AddMonoidWithOne.toOne`	—	—
`ofFinsupp_eq_zero` 📖	mathematical	—	`ofFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SkewMonoidAlgebra` `instZero` `Finsupp` `Finsupp.instZero`	—	—
`ofFinsupp_inj` 📖	mathematical	—	`ofFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`ofFinsupp_injective`
`ofFinsupp_injective` 📖	mathematical	—	`Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SkewMonoidAlgebra` `ofFinsupp`	—	—
`ofFinsupp_neg` 📖	mathematical	—	`ofFinsupp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Finsupp` `Finsupp.instNeg` `SkewMonoidAlgebra` `instNeg`	—	—
`ofFinsupp_one` 📖	mathematical	—	`ofFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `Finsupp.single` `AddMonoidWithOne.toOne` `SkewMonoidAlgebra` `instOne`	—	—
`ofFinsupp_single` 📖	mathematical	—	`ofFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Finsupp.single` `single`	—	—
`ofFinsupp_smul` 📖	mathematical	—	`ofFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Finsupp` `SMulZeroClass.toSMul` `Finsupp.instZero` `Finsupp.smulZeroClass` `SkewMonoidAlgebra` `instZero` `instSMulZeroClass`	—	—
`ofFinsupp_sub` 📖	mathematical	—	`ofFinsupp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Finsupp` `Finsupp.instSub` `SkewMonoidAlgebra` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `instAddGroup`	—	`AddEquiv.map_sub`
`ofFinsupp_sum` 📖	mathematical	—	`ofFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.sum` `Finsupp` `Finsupp.instAddCommMonoid` `sum` `SkewMonoidAlgebra` `instAddCommMonoid`	—	`toFinsupp_injective` `toFinsupp_sum'`
`ofFinsupp_zero` 📖	mathematical	—	`ofFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Finsupp` `Finsupp.instZero` `SkewMonoidAlgebra` `instZero`	—	—
`of_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `instNonAssocSemiring` `MonoidHom.instFunLike` `of` `single` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—
`of_injective` 📖	mathematical	—	`SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `instNonAssocSemiring` `MonoidHom.instFunLike` `of`	—	`NeZero.one` `Finsupp.single_eq_single_iff` `of_apply`
`one_def` 📖	mathematical	—	`SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `instOne` `single` `AddMonoidWithOne.toOne`	—	—
`ringHom_ext` 📖	—	`DFunLike.coe` `RingHom` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instNonAssocSemiring` `RingHom.instFunLike` `single` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—	`single_mul_single` `one_mul` `one_smul` `RingHom.coe_addMonoidHom_injective` `addHom_ext` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `mul_one` `AddMonoidHom.coe_coe` `RingHom.map_mul`
`ringHom_ext'` 📖	—	`RingHom.comp` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instNonAssocSemiring` `singleOneRingHom` `MonoidHom.comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MonoidHomClass.toMonoidHom` `RingHom` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `of`	—	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `ringHom_ext` `RingHom.congr_fun` `DFunLike.congr_fun`
`ringHom_ext'_iff` 📖	mathematical	—	`RingHom.comp` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instNonAssocSemiring` `singleOneRingHom` `MonoidHom.comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MonoidHomClass.toMonoidHom` `RingHom` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `of`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `ringHom_ext'`
`singleAddHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddMonoid` `AddMonoidHom.instFunLike` `singleAddHom` `single`	—	—
`single_add` 📖	mathematical	—	`single` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAdd`	—	`Finsupp.single_add` `toFinsupp_add`
`single_algebraMap_eq_algebraMap_mul_of` 📖	mathematical	—	`single` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DFunLike.coe` `RingHom` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `instSemiring` `instAlgebraOfSMulCommClass` `MonoidHom` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `instNonAssocSemiring` `MonoidHom.instFunLike` `of`	—	`of_apply` `single_mul_single` `one_mul` `MulDistribMulAction.smul_one` `mul_one`
`single_eq_algebraMap_mul_of` 📖	mathematical	—	`single` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `DFunLike.coe` `RingHom` `instSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebraOfSMulCommClass` `Algebra.id` `MonoidHom` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `instNonAssocSemiring` `MonoidHom.instFunLike` `of`	—	`of_apply` `single_mul_single` `one_mul` `MulDistribMulAction.smul_one` `mul_one`
`single_eq_zero` 📖	mathematical	—	`single` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instZero`	—	—
`single_injective` 📖	mathematical	—	`SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `single`	—	`AddEquiv.injective` `Finsupp.single_injective`
`single_left_inj` 📖	mathematical	—	`single`	—	—
`single_mul_single` 📖	mathematical	—	`SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`sum_single_index` `MulZeroClass.zero_mul` `single_zero` `sum_zero` `smul_zero` `MulZeroClass.mul_zero`
`single_nat` 📖	mathematical	—	`single` `AddMonoidWithOne.toAddMonoid` `AddMonoidWithOne.toNatCast` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddMonoidWithOne`	—	`natCast_def`
`single_neg` 📖	mathematical	—	`single` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instNeg`	—	`Finsupp.single_neg` `ofFinsupp_neg`
`single_one_one` 📖	mathematical	—	`single` `AddMonoidWithOne.toAddMonoid` `AddMonoidWithOne.toOne` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instOne`	—	—
`single_zero` 📖	mathematical	—	`single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SkewMonoidAlgebra` `instZero`	—	`Finsupp.single_zero`
`single_zero_right` 📖	mathematical	—	`single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SkewMonoidAlgebra` `instZero`	—	`Finsupp.single_zero`
`smul_of` 📖	mathematical	—	`SkewMonoidAlgebra` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SMulZeroClass.toSMul` `instZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instSMulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `instDistribSMul` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `instNonAssocSemiring` `MonoidHom.instFunLike` `of` `single`	—	`of_apply` `smul_single` `smul_eq_mul` `mul_one`
`smul_single` 📖	mathematical	—	`SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SMulZeroClass.toSMul` `instZero` `instSMulZeroClass` `single`	—	`toFinsupp_injective` `toFinsupp_smul` `Finsupp.smul_single`
`smul_sum` 📖	mathematical	—	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `sum`	—	`Finsupp.smul_sum`
`sum_add` 📖	mathematical	—	`sum` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`Finsupp.sum_add`
`sum_add_index` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`sum` `SkewMonoidAlgebra` `instAdd`	—	`ofFinsupp_add` `eta` `Finsupp.sum_add_index`
`sum_add_index'` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`sum` `SkewMonoidAlgebra` `instAdd`	—	`ofFinsupp_add` `eta` `Finsupp.sum_add_index'`
`sum_congr` 📖	mathematical	`coeff` `AddCommMonoid.toAddMonoid`	`sum`	—	`Finset.sum_congr`
`sum_def` 📖	mathematical	—	`sum` `Finsupp.sum` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `toFinsupp`	—	—
`sum_def'` 📖	mathematical	—	`sum` `Finset.sum` `support` `AddCommMonoid.toAddMonoid` `coeff`	—	—
`sum_ite_eq'` 📖	mathematical	—	`sum` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finset` `Finset.instMembership` `support` `Finset.decidableMem` `coeff`	—	`Finset.sum_ite_eq'`
`sum_mapDomain_index` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`sum` `DFunLike.coe` `AddMonoidHom` `SkewMonoidAlgebra` `instAddMonoid` `AddMonoidHom.instFunLike` `mapDomain`	—	`sum_sum_index` `sum_congr` `sum_single_index`
`sum_mul` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`Finset.sum_mul` `Finset.sum_congr`
`sum_single` 📖	mathematical	—	`sum` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `single`	—	`toFinsupp_injective` `toFinsupp_sum'` `Finsupp.sum_single`
`sum_single_index` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`sum` `single`	—	`Finsupp.sum_single_index`
`sum_smul_index` 📖	mathematical	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `SkewMonoidAlgebra` `SMulZeroClass.toSMul` `instZero` `instSMulZeroClass` `DistribSMul.toSMulZeroClass` `instDistribSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`toFinsupp_smul` `Finsupp.sum_smul_index'`
`sum_smul_index'` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`sum` `SkewMonoidAlgebra` `SMulZeroClass.toSMul` `instZero` `instSMulZeroClass` `DistribSMul.toSMulZeroClass`	—	`toFinsupp_smul` `Finsupp.sum_smul_index'`
`sum_sum_index` 📖	mathematical	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	`sum` `SkewMonoidAlgebra` `instAddCommMonoid`	—	`sum_def` `toFinsupp_sum'` `Finsupp.sum_sum_index`
`sum_zero` 📖	mathematical	—	`sum` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`Finset.sum_const_zero`
`sum_zero_index` 📖	mathematical	—	`sum` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instZero`	—	—
`support_add` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `support` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAdd` `Finset.instUnion`	—	`toFinsupp_add` `Finsupp.support_add`
`support_eq_empty` 📖	mathematical	—	`support` `Finset` `Finset.instEmptyCollection` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instZero`	—	—
`support_ofFinsupp` 📖	mathematical	—	`support` `ofFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Finsupp.support`	—	`support.eq_1`
`support_toFinsupp` 📖	mathematical	—	`Finsupp.support` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `toFinsupp` `support`	—	`support.eq_1`
`support_zero` 📖	mathematical	—	`support` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instZero` `Finset` `Finset.instEmptyCollection`	—	—
`toFinsuppAddEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Finsupp` `instAdd` `Finsupp.instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toFinsuppAddEquiv` `toFinsupp`	—	—
`toFinsuppAddEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SkewMonoidAlgebra` `Finsupp.instAdd` `instAdd` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `toFinsuppAddEquiv` `ofFinsupp`	—	—
`toFinsupp_add` 📖	mathematical	—	`toFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SkewMonoidAlgebra` `instAdd` `Finsupp` `Finsupp.instAdd`	—	`ofFinsupp_add`
`toFinsupp_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Finsupp.instFunLike` `toFinsupp` `coeff`	—	—
`toFinsupp_eq_single_one_one_iff` 📖	mathematical	—	`toFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `Finsupp.single` `AddMonoidWithOne.toOne` `SkewMonoidAlgebra` `instOne`	—	—
`toFinsupp_eq_zero` 📖	mathematical	—	`toFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Finsupp` `Finsupp.instZero` `SkewMonoidAlgebra` `instZero`	—	—
`toFinsupp_inj` 📖	mathematical	—	`toFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`toFinsupp_injective`
`toFinsupp_injective` 📖	mathematical	—	`SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Finsupp` `toFinsupp`	—	—
`toFinsupp_mapDomain` 📖	mathematical	—	`toFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `AddMonoidHom` `SkewMonoidAlgebra` `instAddMonoid` `AddMonoidHom.instFunLike` `mapDomain` `Finsupp.mapDomain`	—	`toFinsupp_sum'`
`toFinsupp_neg` 📖	mathematical	—	`toFinsupp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `SkewMonoidAlgebra` `instNeg` `Finsupp` `Finsupp.instNeg`	—	`AddEquiv.map_neg`
`toFinsupp_one` 📖	mathematical	—	`toFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `SkewMonoidAlgebra` `instOne` `Finsupp.single` `AddMonoidWithOne.toOne`	—	—
`toFinsupp_single` 📖	mathematical	—	`toFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `single` `Finsupp.single`	—	—
`toFinsupp_smul` 📖	mathematical	—	`toFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SkewMonoidAlgebra` `SMulZeroClass.toSMul` `instZero` `instSMulZeroClass` `Finsupp` `Finsupp.instZero` `Finsupp.smulZeroClass`	—	`ofFinsupp_smul`
`toFinsupp_sub` 📖	mathematical	—	`toFinsupp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `SkewMonoidAlgebra` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `instAddGroup` `Finsupp` `Finsupp.instSub`	—	`AddEquiv.map_sub`
`toFinsupp_sum'` 📖	mathematical	—	`toFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `sum` `SkewMonoidAlgebra` `instAddCommMonoid` `Finsupp.sum` `Finsupp` `Finsupp.instAddCommMonoid`	—	`map_sum` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass`
`toFinsupp_zero` 📖	mathematical	—	`toFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SkewMonoidAlgebra` `instZero` `Finsupp` `Finsupp.instZero`	—	—

SkewMonoidAlgebra.DistribMulActionHom

Definitions

Name	Category	Theorems
`single` 📖	CompOp	2 math math: `SkewMonoidAlgebra.distribMulActionHom_ext'_iff`, `single_toFun`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`single_toFun` 📖	mathematical	—	`DFunLike.coe` `DistribMulActionHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MonoidHom.id` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `AddCommMonoid.toAddMonoid` `SkewMonoidAlgebra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SkewMonoidAlgebra.instAddMonoid` `SkewMonoidAlgebra.instDistribMulAction` `DistribMulActionHom.instFunLike` `single` `ZeroHom.toFun` `AddMonoidHom.toZeroHom` `SkewMonoidAlgebra.singleAddHom`	—	—

(root)

Definitions

Name	Category	Theorems
`SkewMonoidAlgebra` 📖	CompData	144 math math: `SkewMonoidAlgebra.mapDomain_smul`, `SkewMonoidAlgebra.ofFinsupp_eq_zero`, `SkewMonoidAlgebra.instNontrivialOfNonempty`, `SkewMonoidAlgebra.sum_add_index`, `SkewMonoidAlgebra.domCongr_support`, `SkewMonoidAlgebra.single_neg`, `IsSMulRegular.skewMonoidAlgebra`, `SkewMonoidAlgebra.ofFinsupp_zero`, `SkewMonoidAlgebra.ofFinsupp_smul`, `SkewMonoidAlgebra.erase_apply_toFinsupp`, `SkewMonoidAlgebra.single_injective`, `SkewMonoidAlgebra.coeff_single_one_mul`, `SkewMonoidAlgebra.toFinsupp_smul`, `SkewMonoidAlgebra.algHom_ext'_iff`, `SkewMonoidAlgebra.lift_apply'`, `SkewMonoidAlgebra.support_single_mul`, `SkewMonoidAlgebra.coeff_single_mul_of_not_exists_mul`, `SkewMonoidAlgebra.coeff_erase_same`, `SkewMonoidAlgebra.single_algebraMap_eq_algebraMap_mul_of`, `SkewMonoidAlgebra.mapDomain_one`, `SkewMonoidAlgebra.smul_of`, `SkewMonoidAlgebra.toFinsupp_eq_single_one_one_iff`, `SkewMonoidAlgebra.support_mul_single`, `SkewMonoidAlgebra.domCongrAlg_apply`, `SkewMonoidAlgebra.support_one`, `SkewMonoidAlgebra.coeff_erase_ne`, `SkewMonoidAlgebra.sum_add_index'`, `SkewMonoidAlgebra.support_one_subset`, `SkewMonoidAlgebra.mapDomain_mul`, `SkewMonoidAlgebra.mapDomain_single`, `SkewMonoidAlgebra.ofFinsupp_sum`, `SkewMonoidAlgebra.support_sum`, `SkewMonoidAlgebra.single_eq_zero`, `SkewMonoidAlgebra.comapSMul_def`, `SkewMonoidAlgebra.coeff_sum`, `SkewMonoidAlgebra.one_def`, `SkewMonoidAlgebra.support_eq_empty`, `SkewMonoidAlgebra.addHom_ext_iff`, `SkewMonoidAlgebra.lift_of`, `SkewMonoidAlgebra.lift_single`, `SkewMonoidAlgebra.lift_apply`, `SkewMonoidAlgebra.nonUnitalAlgHom_ext'_iff`, `SkewMonoidAlgebra.coeff_mul_single_of_not_exists_mul`, `SkewMonoidAlgebra.toFinsupp_sub`, `SkewMonoidAlgebra.coeff_mul_right`, `SkewMonoidAlgebra.of_apply`, `SkewMonoidAlgebra.instFaithfulSMul`, `SkewMonoidAlgebra.sum_single`, `SkewMonoidAlgebra.toFinsuppAddEquiv_apply`, `SkewMonoidAlgebra.lift_unique`, `SkewMonoidAlgebra.domCongrAlg_toAlgHom`, `SkewMonoidAlgebra.sum_smul_index'`, `SkewMonoidAlgebra.support_mul_single_eq_image`, `SkewMonoidAlgebra.single_zero`, `SkewMonoidAlgebra.single_mul_single`, `SkewMonoidAlgebra.support_single_mul_eq_image`, `SkewMonoidAlgebra.coeff_one_one`, `SkewMonoidAlgebra.ofFinsupp_injective`, `SkewMonoidAlgebra.instIsScalarTower`, `SkewMonoidAlgebra.comapSMul_single`, `SkewMonoidAlgebra.coeff_zero`, `SkewMonoidAlgebra.domCongr_refl`, `SkewMonoidAlgebra.coe_algebraMap`, `SkewMonoidAlgebra.liftNC_one`, `SkewMonoidAlgebra.instFree`, `SkewMonoidAlgebra.update_eq_erase_add_single`, `SkewMonoidAlgebra.mapDomain_id`, `SkewMonoidAlgebra.addHom_ext'_iff`, `SkewMonoidAlgebra.coeff_mul`, `SkewMonoidAlgebra.smul_single`, `SkewMonoidAlgebra.toFinsuppAddEquiv_symm_apply`, `SkewMonoidAlgebra.toFinsupp_injective`, `SkewMonoidAlgebra.toFinsupp_neg`, `SkewMonoidAlgebra.support_add`, `SkewMonoidAlgebra.coeff_mul_antidiagonal_finsum`, `SkewMonoidAlgebra.toFinsupp_zero`, `SkewMonoidAlgebra.zero_update`, `SkewMonoidAlgebra.ofFinsupp_neg`, `SkewMonoidAlgebra.lift_unique'`, `SkewMonoidAlgebra.single_zero_right`, `SkewMonoidAlgebra.toFinsupp_one`, `SkewMonoidAlgebra.single_add`, `SkewMonoidAlgebra.sum_smul_index`, `SkewMonoidAlgebra.ofFinsupp_add`, `SkewMonoidAlgebra.support_zero`, `SkewMonoidAlgebra.support_mul_single_subset`, `SkewMonoidAlgebra.toFinsupp_add`, `SkewMonoidAlgebra.coeff_mul_single`, `SkewMonoidAlgebra.support_mul`, `SkewMonoidAlgebra.mapDomainAlgHom_apply`, `SkewMonoidAlgebra.lhom_ext'_iff`, `SkewMonoidAlgebra.liftNC_mul`, `SkewMonoidAlgebra.coeff_one`, `SkewMonoidAlgebra.single_one_one`, `SkewMonoidAlgebra.sum_mapDomain_index`, `SkewMonoidAlgebra.coeff_mul_single_one`, `SkewMonoidAlgebra.toFinsupp_mapDomain`, `SkewMonoidAlgebra.update_zero_eq_erase`, `SkewMonoidAlgebra.ofFinsupp_eq_one`, `SkewMonoidAlgebra.sum_zero_index`, `SkewMonoidAlgebra.support_neg`, `SkewMonoidAlgebra.of_injective`, `SkewMonoidAlgebra.natCast_def`, `SkewMonoidAlgebra.isScalarTower_self`, `SkewMonoidAlgebra.sum_sum_index`, `SkewMonoidAlgebra.liftNC_single`, `SkewMonoidAlgebra.intCast_def`, `SkewMonoidAlgebra.erase_single`, `SkewMonoidAlgebra.support_single_mul_subset`, `SkewMonoidAlgebra.single_nat`, `SkewMonoidAlgebra.instSMulCommClass`, `IsSMulRegular.skewMonoidAlgebra_iff`, `SkewMonoidAlgebra.coeff_mul_antidiagonal_of_finset`, `SkewMonoidAlgebra.ofFinsupp_sub`, `SkewMonoidAlgebra.instIsCentralScalar`, `SkewMonoidAlgebra.single_eq_algebraMap_mul_of`, `SkewMonoidAlgebra.distribMulActionHom_ext'_iff`, `SkewMonoidAlgebra.coeff_mul_left`, `SkewMonoidAlgebra.coeff_mul_single_aux`, `SkewMonoidAlgebra.coeff_injective`, `SkewMonoidAlgebra.toFinsupp_eq_zero`, `SkewMonoidAlgebra.ringHom_ext'_iff`, `SkewMonoidAlgebra.ofFinsupp_one`, `SkewMonoidAlgebra.domCongr_apply`, `SkewMonoidAlgebra.domCongr_single`, `SkewMonoidAlgebra.coeff_smul`, `SkewMonoidAlgebra.single_add_erase`, `SkewMonoidAlgebra.coeff_single_mul_aux`, `SkewMonoidAlgebra.mem_span_support`, `SkewMonoidAlgebra.lift_def`, `SkewMonoidAlgebra.DistribMulActionHom.single_toFun`, `SkewMonoidAlgebra.equivMapDomain_eq_mapDomain`, `SkewMonoidAlgebra.domCongr_symm`, `SkewMonoidAlgebra.mapDomain_apply`, `SkewMonoidAlgebra.toFinsupp_sum'`, `SkewMonoidAlgebra.singleAddHom_apply`, `SkewMonoidAlgebra.coeff_single_mul`, `SkewMonoidAlgebra.liftNC_smul`, `SkewMonoidAlgebra.coeff_add`, `SkewMonoidAlgebra.coeff_erase_apply`, `SkewMonoidAlgebra.support_erase`, `SkewMonoidAlgebra.mul_def`, `SkewMonoidAlgebra.lift_symm_apply`, `SkewMonoidAlgebra.mapDomain_comp`

---

← Back to Index