Defs

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

Statistics

Metric	Count
Definitions curryLinearEquiv, finsuppProdLEquiv, lapply, lcomapDomain, linearEquivFunOnFinite, lmapDomain, lsingle, lsubtypeDomain, linearEquiv, linearEquiv, linearMap, ringEquivEndFinsupp, ringHomEndFinsupp, subsingletonEquiv	14
Theorems coe_lmapDomain, curryLinearEquiv_apply, curryLinearEquiv_symm_apply, curryLinearEquiv_symm_apply_apply, finsuppProdLEquiv_symm_apply_apply, instFaithfulSMulOfNonempty, lapply_apply, lapply_comp_lsingle_of_ne, lapply_comp_lsingle_same, lcomapDomain_apply, leftInverse_lcomapDomain_mapDomain, lhom_ext, lhom_ext', lhom_ext'_iff, linearEquivFunOnFinite_apply, linearEquivFunOnFinite_single, linearEquivFunOnFinite_symm_apply, linearEquivFunOnFinite_symm_coe, linearEquivFunOnFinite_symm_single, lmapDomain_apply, lmapDomain_comp, lmapDomain_id, lsingle_apply, lsubtypeDomain_apply, coe_linearEquiv, linearEquiv_symm, toLinearMap_linearEquiv, linearEquiv_apply, linearEquiv_refl, linearEquiv_symm, linearEquiv_toAddEquiv, linearEquiv_toLinearMap, linearEquiv_trans, linearMap_apply, linearMap_comp, linearMap_id, linearMap_toAddMonoidHom, ringEquivEndFinsupp_apply_apply_apply, ringEquivEndFinsupp_apply_apply_support, ringEquivEndFinsupp_symm_apply_apply, ringHomEndFinsupp_apply_apply, ringHomEndFinsupp_surjective, subsingletonEquiv_apply, subsingletonEquiv_symm_apply	44
Total	58

Finsupp

Definitions

Name	Category	Theorems
curryLinearEquiv 📖	CompOp	8 math math: curryLinearEquiv_symm_apply_apply, linearCombination_smul, Rep.leftRegularTensorTrivialIsoFree_inv_hom, curryLinearEquiv_apply, Rep.freeLift_hom, finsuppProdLEquiv_symm_apply_apply, Rep.leftRegularTensorTrivialIsoFree_hom_hom, curryLinearEquiv_symm_apply
finsuppProdLEquiv 📖	CompOp	—
lapply 📖	CompOp	10 math math: TensorProduct.finsuppRight_apply, iInf_ker_lapply_le_bot, TensorProduct.finsuppScalarRight_apply, comul_comp_lapply, TensorProduct.finsuppLeft_apply, lapply_comp_lsingle_same, lapply_apply, lapply_comp_lsingle_of_ne, lsingle_range_le_ker_lapply, TensorProduct.finsuppScalarLeft_apply
lcomapDomain 📖	CompOp	3 math math: leftInverse_lcomapDomain_mapDomain, lcomapDomain_apply, lcomapDomain_eq_linearProjOfIsCompl
linearEquivFunOnFinite 📖	CompOp	7 math math: linearEquivFunOnFinite_symm_coe, linearEquivFunOnFinite_symm_apply, linearEquivFunOnFinite_single, linearEquivFunOnFinite_apply, linearEquivFunOnFinite_symm_single, linearCombination_eq_fintype_linearCombination, linearCombination_eq_fintype_linearCombination_apply
lmapDomain 📖	CompOp	29 math math: Rep.coe_linearization_obj_ρ, PolynomialModule.smul_def, lmapDomain_id, lmapDomain_linearCombination, lmapDomain_comp, supported_comap_lmapDomain, groupHomology.mapCycles₁_comp_i_apply, KaehlerDifferential.ker_map, isCompl_range_lmapDomain_span, KaehlerDifferential.kerTotal_map, Rep.linearization_obj_ρ, coe_lmapDomain, linearCombination_comp, groupHomology.chainsMap_f_hom, KaehlerDifferential.ker_map_of_surjective, mapDomain.toLinearMap_linearEquiv, groupHomology.mapCycles₂_comp_i_apply, range_lmapDomain, linearCombination_comp_lmapDomain, Module.Basis.constr_def, Representation.ind_apply, lmapDomain_disjoint_ker, KaehlerDifferential.kerTotal_map', lcomapDomain_eq_linearProjOfIsCompl, lmapDomain_apply, Rep.linearization_map_hom, lmapDomain_supported, groupHomology.chainsMap_f, Representation.ofMulAction_def
lsingle 📖	CompOp	23 math math: Representation.finsupp_apply, AddMonoidAlgebra.grade_eq_lsingle_range, lcoeFun_comp_lsingle, counit_comp_lsingle, lhom_ext'_iff, AddMonoidAlgebra.mem_grade_iff', lapply_comp_lsingle_same, groupHomology.lsingle_comp_chainsMap_f, comul_single, lapply_comp_lsingle_of_ne, groupHomology.inhomogeneousChains.ext_iff, disjoint_lsingle_lsingle, lsum_comp_lsingle, span_single_image, lsingle_range_le_ker_lapply, comul_comp_lsingle, groupHomology.lsingle_comp_chainsMap_f_assoc, ker_lsingle, iSupIndep_range_lsingle, Rep.linearization_ε_hom, lsingle_apply, lsum_symm_apply, iSup_lsingle_range
lsubtypeDomain 📖	CompOp	1 math math: lsubtypeDomain_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_lmapDomain 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module LinearMap.instFunLike lmapDomain mapDomain	—	—
curryLinearEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instZero instAddCommMonoid module EquivLike.toFunLike LinearEquiv.instEquivLike curryLinearEquiv curry	—	RingHomInvPair.ids
curryLinearEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instZero instAddCommMonoid module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm curryLinearEquiv uncurry	—	RingHomInvPair.ids
curryLinearEquiv_symm_apply_apply 📖	mathematical	—	DFunLike.coe Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instZero instAddCommMonoid module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm curryLinearEquiv	—	RingHomInvPair.ids
finsuppProdLEquiv_symm_apply_apply 📖	mathematical	—	DFunLike.coe Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instZero instAddCommMonoid module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm curryLinearEquiv	—	curryLinearEquiv_symm_apply_apply
instFaithfulSMulOfNonempty 📖	mathematical	—	FaithfulSMul Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul instZero smulZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	FaithfulSMul.of_injective SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass single_injective
lapply_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module LinearMap.instFunLike lapply instFunLike	—	—
lapply_comp_lsingle_of_ne 📖	mathematical	—	LinearMap.comp Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids lapply lsingle LinearMap LinearMap.instZero	—	LinearMap.ext RingHomCompTriple.ids single_eq_of_ne'
lapply_comp_lsingle_same 📖	mathematical	—	LinearMap.comp Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids lapply lsingle LinearMap.id	—	LinearMap.ext RingHomCompTriple.ids single_eq_same
lcomapDomain_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module LinearMap.instFunLike lcomapDomain comapDomain	—	—
leftInverse_lcomapDomain_mapDomain 📖	mathematical	—	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instAddCommMonoid module LinearMap.instFunLike lcomapDomain mapDomain	—	comapDomain_mapDomain
lhom_ext 📖	—	DFunLike.coe LinearMap Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module LinearMap.instFunLike single	—	—	LinearMap.toAddMonoidHom_injective addHom_ext
lhom_ext' 📖	—	LinearMap.comp Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids lsingle	—	—	RingHomCompTriple.ids lhom_ext LinearMap.congr_fun
lhom_ext'_iff 📖	mathematical	—	LinearMap.comp Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids lsingle	—	RingHomCompTriple.ids lhom_ext'
linearEquivFunOnFinite_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid Pi.addCommMonoid module Pi.Function.module EquivLike.toFunLike LinearEquiv.instEquivLike linearEquivFunOnFinite instFunLike	—	RingHomInvPair.ids
linearEquivFunOnFinite_single 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid Pi.addCommMonoid module Pi.Function.module EquivLike.toFunLike LinearEquiv.instEquivLike linearEquivFunOnFinite single Pi.single	—	equivFunOnFinite_single
linearEquivFunOnFinite_symm_apply 📖	mathematical	—	DFunLike.coe Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Pi.addCommMonoid instAddCommMonoid Pi.Function.module module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm linearEquivFunOnFinite	—	RingHomInvPair.ids
linearEquivFunOnFinite_symm_coe 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Pi.addCommMonoid instAddCommMonoid Pi.Function.module module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm linearEquivFunOnFinite instFunLike	—	LinearEquiv.symm_apply_apply RingHomInvPair.ids
linearEquivFunOnFinite_symm_single 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Pi.addCommMonoid instAddCommMonoid Pi.Function.module module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm linearEquivFunOnFinite Pi.single single	—	equivFunOnFinite_symm_single
lmapDomain_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module LinearMap.instFunLike lmapDomain mapDomain	—	—
lmapDomain_comp 📖	mathematical	—	lmapDomain LinearMap.comp Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	LinearMap.ext RingHomCompTriple.ids mapDomain_comp
lmapDomain_id 📖	mathematical	—	lmapDomain LinearMap.id Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module	—	LinearMap.ext mapDomain_id
lsingle_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module LinearMap.instFunLike lsingle single	—	—
lsubtypeDomain_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Set.Elem instAddCommMonoid module LinearMap.instFunLike lsubtypeDomain subtypeDomain Set Set.instMembership	—	—

Finsupp.mapDomain

Definitions

Name	Category	Theorems
linearEquiv 📖	CompOp	3 math math: coe_linearEquiv, toLinearMap_linearEquiv, linearEquiv_symm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_linearEquiv 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module EquivLike.toFunLike LinearEquiv.instEquivLike linearEquiv Finsupp.mapDomain Equiv Equiv.instEquivLike	—	RingHomInvPair.ids
linearEquiv_symm 📖	mathematical	—	LinearEquiv.symm Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids linearEquiv Equiv.symm	—	RingHomInvPair.ids
toLinearMap_linearEquiv 📖	mathematical	—	LinearEquiv.toLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module linearEquiv Finsupp.lmapDomain DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	RingHomInvPair.ids

Finsupp.mapRange

Definitions

Name	Category	Theorems
linearEquiv 📖	CompOp	7 math math: linearEquiv_refl, linearEquiv_toAddEquiv, linearEquiv_symm, linearEquiv_toLinearMap, linearEquiv_apply, linearEquiv_trans, Module.Basis.mapCoeffs_repr
linearMap 📖	CompOp	21 math math: IsBaseChange.finsuppPow, Finsupp.linearCombination_smul, Finsupp.range_mapRange_linearMap, Finsupp.ker_mapRange, groupHomology.mapCycles₁_comp_i_apply, KaehlerDifferential.ker_map, instIsLocalizedModuleFinsuppLinearMap, IsLocalizedModule.map_linearCombination, linearMap_apply, KaehlerDifferential.kerTotal_map, linearEquiv_toLinearMap, groupHomology.chainsMap_id_f_hom_eq_mapRange, linearMap_comp, linearMap_id, groupHomology.chainsMap_f_hom, linearMap_toAddMonoidHom, KaehlerDifferential.ker_map_of_surjective, IsBaseChange.basis_repr_comp, groupHomology.mapCycles₂_comp_i_apply, KaehlerDifferential.kerTotal_map', groupHomology.chainsMap_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
linearEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module EquivLike.toFunLike LinearEquiv.instEquivLike linearEquiv Finsupp.mapRange LinearEquiv.map_zero	—	—
linearEquiv_refl 📖	mathematical	—	linearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearEquiv.refl Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module	—	LinearEquiv.ext RingHomInvPair.ids Finsupp.mapRange_id
linearEquiv_symm 📖	mathematical	—	LinearEquiv.symm Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module linearEquiv	—	LinearEquiv.ext
linearEquiv_toAddEquiv 📖	mathematical	—	LinearEquiv.toAddEquiv Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module linearEquiv addEquiv	—	AddEquiv.ext
linearEquiv_toLinearMap 📖	mathematical	—	LinearEquiv.toLinearMap Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module linearEquiv linearMap	—	LinearMap.ext
linearEquiv_trans 📖	mathematical	—	linearEquiv LinearEquiv.trans Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module	—	LinearEquiv.ext Finsupp.mapRange_comp LinearEquiv.map_zero
linearMap_apply 📖	mathematical	—	DFunLike.coe LinearMap Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module LinearMap.instFunLike linearMap Finsupp.mapRange LinearMap.map_zero	—	—
linearMap_comp 📖	mathematical	—	linearMap LinearMap.comp Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module	—	LinearMap.ext Finsupp.mapRange_comp LinearMap.map_zero
linearMap_id 📖	mathematical	—	linearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.id Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module	—	LinearMap.ext Finsupp.mapRange_id
linearMap_toAddMonoidHom 📖	mathematical	—	LinearMap.toAddMonoidHom Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module linearMap addMonoidHom	—	AddMonoidHom.ext

Module

Definitions

Name	Category	Theorems
subsingletonEquiv 📖	CompOp	2 math math: subsingletonEquiv_symm_apply, subsingletonEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
subsingletonEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike LinearEquiv.instEquivLike subsingletonEquiv Finsupp.instZero	—	RingHomInvPair.ids
subsingletonEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm subsingletonEquiv AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	RingHomInvPair.ids

Module.End

Definitions

Name	Category	Theorems
ringEquivEndFinsupp 📖	CompOp	3 math math: ringEquivEndFinsupp_apply_apply_apply, ringEquivEndFinsupp_apply_apply_support, ringEquivEndFinsupp_symm_apply_apply
ringHomEndFinsupp 📖	CompOp	2 math math: ringHomEndFinsupp_apply_apply, ringHomEndFinsupp_surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ringEquivEndFinsupp_apply_apply_apply 📖	mathematical	—	DFunLike.coe Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instFunLike LinearMap Module.End Finsupp.instAddCommMonoid Finsupp.module instSemiring RingHom.id Semiring.toNonAssocSemiring applyModule LinearMap.instFunLike RingEquiv instMul LinearMap.instAdd EquivLike.toFunLike RingEquiv.instEquivLike ringEquivEndFinsupp	—	—
ringEquivEndFinsupp_apply_apply_support 📖	mathematical	—	Finsupp.support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe LinearMap Module.End Finsupp Finsupp.instAddCommMonoid Finsupp.module instSemiring RingHom.id Semiring.toNonAssocSemiring applyModule LinearMap.instFunLike RingEquiv instMul LinearMap.instAdd EquivLike.toFunLike RingEquiv.instEquivLike ringEquivEndFinsupp Finsupp.onFinset_support Finsupp.instFunLike	—	—
ringEquivEndFinsupp_symm_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap Module.End instSemiring RingHom.id Semiring.toNonAssocSemiring applyModule LinearMap.instFunLike RingEquiv Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module instMul LinearMap.instAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm ringEquivEndFinsupp Finsupp.instFunLike Finsupp.single	—	—
ringHomEndFinsupp_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap Module.End Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module instSemiring RingHom.id Semiring.toNonAssocSemiring applyModule LinearMap.instFunLike RingHom RingHom.instFunLike ringHomEndFinsupp AddMonoidHom Finsupp.instAddZeroClass AddMonoidHom.instFunLike Finsupp.mapRange.addMonoidHom AddMonoidHomClass.toAddMonoidHom	—	—
ringHomEndFinsupp_surjective 📖	mathematical	—	Module.End instSemiring applyModule Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike ringHomEndFinsupp	—	isEmpty_or_nonempty Unique.instSubsingleton Equiv.right_inv

---

← Back to Index