LinearCombination

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

Statistics

Metric	Count
Definitions addSingleEquiv, bilinearCombination, linearCombination, linearCombinationOn, bilinearCombination, linearCombination, repr	7
Theorems apply_linearCombination, apply_linearCombination_id, bilinearCombination_apply, linearCombinationOn_range, linearCombination_apply, linearCombination_apply_of_mem_supported, linearCombination_comapDomain, linearCombination_comp, linearCombination_comp_addSingleEquiv, linearCombination_comp_lmapDomain, linearCombination_embDomain, linearCombination_eq_fintype_linearCombination, linearCombination_eq_fintype_linearCombination_apply, linearCombination_equivMapDomain, linearCombination_fin_zero, linearCombination_id_surjective, linearCombination_linearCombination, linearCombination_linear_comp, linearCombination_mapDomain, linearCombination_onFinset, linearCombination_option, linearCombination_range, linearCombination_restrict, linearCombination_single, linearCombination_single_index, linearCombination_smul, linearCombination_surjective, linearCombination_unique, linearCombination_zero, linearCombination_zero_apply, lmapDomain_linearCombination, mem_span_iff_linearCombination, mem_span_image_iff_linearCombination, mem_span_range_iff_exists_finsupp, range_linearCombination, span_eq_range_linearCombination, span_image_eq_map_linearCombination, bilinearCombination_apply, bilinearCombination_apply_single, linearCombination_apply, linearCombination_apply_single, mem_span_image_iff_exists_fun, range_linearCombination, map_finsupp_linearCombination, finsupp_linearCombination_repr, repr_def, mem_span_finset, mem_span_finset', mem_span_iff_exists_finset_subset, mem_span_iff_of_fintype, mem_span_image_iff_exists_fun, mem_span_range_iff_exists_fun, mem_span_set, mem_span_set', span_eq_iUnion_nat, top_le_span_range_iff_forall_exists_fun, span_range_eq_top_iff_surjective_finsuppLinearCombination, span_range_eq_top_iff_surjective_fintypeLinearCombination	58
Total	65

Finsupp

Definitions

Name	Category	Theorems
addSingleEquiv 📖	CompOp	1 math math: linearCombination_comp_addSingleEquiv
bilinearCombination 📖	CompOp	1 math math: bilinearCombination_apply
linearCombination 📖	CompOp	101 math math: linearCombination_apply_of_mem_supported, Orthonormal.inner_left_finsupp, QuadraticMap.sum_polar_sub_repr_sq, Module.Basis.toDual_linearCombination_left, linearCombination_id_surjective, LinearIndependent.linearCombination_repr, Span.repr_def, linearIndependent_iff_injective_finsuppLinearCombination, linearCombination_zero_apply, mem_span_iff_linearCombination, linearIndependent_iff_ker, linearCombination_smul, lmapDomain_linearCombination, linearCombination_one_tmul, KaehlerDifferential.kerTotal_eq, span_image_eq_map_linearCombination, Representation.leftRegular_norm_eq_zero_iff, linearCombination_linear_comp, IsBaseChange.of_basis, Module.Basis.repr_linearCombination, Algebra.Generators.H1Cotangent.δAux_toAlgHom, linearCombination_single_index, LinearIndependent.linearCombinationEquiv_apply_coe, LinearIndependent.linearCombination_comp_repr, Module.Basis.linearCombination_dualBasis, KaehlerDifferential.ker_map, IsLocalizedModule.map_linearCombination, linearIndepOn_iff_disjoint, Orthonormal.inner_finsupp_eq_sum_right, span_eq_range_linearCombination, MvPolynomial.combinatorial_nullstellensatz_exists_linearCombination, Algebra.Presentation.differentials.comm₂₃', linearCombination_apply, Submodule.mulRightMap_eq_mulMap_comp, linearCombination_embDomain, linearCombination_single, Orthonormal.inner_right_finsupp, linearCombination_unique, linearCombination_mapDomain, Span.finsupp_linearCombination_repr, LinearIndependent.linearCombinationEquiv_symm_apply, linearCombination_range, Orthonormal.inner_finsupp_eq_sum_left, LinearIndependent.finsuppLinearCombination_injective, Representation.ker_leftRegular_norm_eq, linearCombination_restrict, linearCombination_comp, range_linearCombination, bilinearCombination_apply, apply_linearCombination, Module.Basis.end_repr_symm_apply, linearCombination_comp_addSingleEquiv, MonomialOrder.div_set, Submodule.mulLeftMap_eq_mulMap_comp, KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination, Rep.coindVEquiv_apply_hom, Module.Basis.linearCombination_repr, Module.FinitePresentation.out, Module.Basis.linearCombination_coord, Representation.FiniteCyclicGroup.coinvariantsKer_leftRegular_eq_ker, Module.projective_def', Module.Basis.coe_repr_symm, linearCombination_fin_zero, linearCombination_equivMapDomain, Orthonormal.inner_finsupp_eq_zero, QuadraticMap.apply_linearCombination', linearCombination_linearCombination, linearCombination_option, linearCombination_eq_fintype_linearCombination, KaehlerDifferential.ker_map_of_surjective, Module.Basis.linearMap_repr_symm_apply, span_range_eq_top_iff_surjective_finsuppLinearCombination, Representation.leftRegular_norm_apply, Module.Basis.toDual_linearCombination_right, QuadraticMap.apply_linearCombination, Module.projective_def, Rep.freeLift_hom, MonomialOrder.div, linearCombination_surjective, linearCombination_comp_lmapDomain, mem_span_image_iff_linearCombination, Module.Basis.constr_def, QuadraticMap.sum_repr_sq_add_sum_repr_mul_polar, Module.DualBases.lc_def, linearCombination_comapDomain, Module.Basis.repr_symm_apply, apply_linearCombination_id, Module.Projective.out, linearCombination_eq_fintype_linearCombination_apply, mem_finsuppAffineCoords_iff_linearCombination, linearDepOn_iff', KaehlerDifferential.quotKerTotalEquiv_apply, linearCombination_zero, linearDepOn_iff'ₛ, LinearMap.map_finsupp_linearCombination, Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination, lsum_comp_mapRange_toSpanSingleton, KaehlerDifferential.linearCombination_surjective, linearCombination_onFinset, Module.Relations.Solution.linearCombination_var_relation, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply
linearCombinationOn 📖	CompOp	4 math math: linearCombinationOn_range, linearCombination_restrict, linearIndepOn_iff_linearCombinationOnₛ, linearIndepOn_iff_linearCombinationOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_linearCombination 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule linearCombination	—	RingHomCompTriple.ids linearCombination_linear_comp
apply_linearCombination_id 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule linearCombination	—	apply_linearCombination
bilinearCombination_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule Pi.addCommMonoid LinearMap.addCommMonoid Pi.Function.module LinearMap.module LinearMap.instFunLike bilinearCombination linearCombination	—	—
linearCombinationOn_range 📖	mathematical	—	LinearMap.range Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Submodule instAddCommMonoid module Semiring.toModule SetLike.instMembership Submodule.setLike supported Submodule.span Set.image Submodule.addCommMonoid Submodule.module RingHom.id RingHomSurjective.ids linearCombinationOn Top.top Submodule.instTop	—	RingHomSurjective.ids linearCombinationOn.eq_1 LinearMap.range_eq_map LinearMap.map_codRestrict LinearMap.range_le_iff_comap Submodule.range_subtype Submodule.map_top LinearMap.range_comp Eq.le span_image_eq_map_linearCombination
linearCombination_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule LinearMap.instFunLike linearCombination sum SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—
linearCombination_apply_of_mem_supported 📖	mathematical	Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Submodule AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instAddCommMonoid module Semiring.toModule SetLike.instMembership Submodule.setLike supported SetLike.coe Finset Finset.instSetLike	DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike linearCombination Finset.sum SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instFunLike	—	Finset.sum_subset notMem_support_iff zero_smul
linearCombination_comapDomain 📖	mathematical	Set.InjOn Set.preimage SetLike.coe Finset Finset.instSetLike support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	DFunLike.coe LinearMap RingHom.id Finsupp instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule LinearMap.instFunLike linearCombination comapDomain Finset.sum Finset.preimage SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instFunLike	—	linearCombination_apply
linearCombination_comp 📖	mathematical	—	linearCombination LinearMap.comp Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass instAddCommMonoid module Semiring.toModule RingHom.id RingHomCompTriple.ids lmapDomain	—	lhom_ext' RingHomCompTriple.ids LinearMap.ext_ring sum_single_index zero_smul one_smul mapDomain_single
linearCombination_comp_addSingleEquiv 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	LinearMap.comp Finsupp NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ring.toSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddCommGroup.toAddCommMonoid module Semiring.toModule RingHom.id RingHomCompTriple.ids linearCombination LinearEquiv.toLinearMap RingHomInvPair.ids addSingleEquiv Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	lhom_ext' RingHomCompTriple.ids RingHomInvPair.ids LinearMap.ext_ring linearCombination_single smul_add one_smul map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass
linearCombination_comp_lmapDomain 📖	mathematical	—	LinearMap.comp Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass instAddCommMonoid module Semiring.toModule RingHom.id RingHomCompTriple.ids linearCombination lmapDomain	—	lhom_ext' RingHomCompTriple.ids LinearMap.ext_ring mapDomain_single linearCombination_single one_smul
linearCombination_embDomain 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule LinearMap.instFunLike linearCombination embDomain Function.Embedding Function.instFunLikeEmbedding	—	Finset.sum_congr embDomain_apply dite_smul zero_smul Finset.sum_map Function.instEmbeddingLikeEmbedding Classical.choose_eq
linearCombination_eq_fintype_linearCombination 📖	mathematical	—	LinearMap.comp Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instAddCommMonoid Pi.Function.module Semiring.toModule module RingHom.id RingHomCompTriple.ids linearCombination LinearEquiv.toLinearMap RingHomInvPair.ids AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid LinearEquiv.symm linearEquivFunOnFinite Finite.of_fintype Fintype.linearCombination	—	LinearMap.ext RingHomCompTriple.ids RingHomInvPair.ids Finite.of_fintype linearCombination_eq_fintype_linearCombination_apply
linearCombination_eq_fintype_linearCombination_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule LinearMap.instFunLike linearCombination LinearEquiv RingHomInvPair.ids AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Pi.addCommMonoid Pi.Function.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm linearEquivFunOnFinite Finite.of_fintype Fintype.linearCombination	—	Finset.sum_subset RingHomInvPair.ids Finite.of_fintype Finset.subset_univ notMem_support_iff zero_smul
linearCombination_equivMapDomain 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule LinearMap.instFunLike linearCombination equivMapDomain Equiv EquivLike.toFunLike Equiv.instEquivLike	—	equivMapDomain_eq_mapDomain linearCombination_mapDomain
linearCombination_fin_zero 📖	mathematical	—	linearCombination LinearMap RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule LinearMap.instZero	—	lhom_ext' LinearMap.ext_ring RingHomCompTriple.ids
linearCombination_id_surjective 📖	mathematical	—	Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe LinearMap RingHom.id instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule LinearMap.instFunLike linearCombination	—	linearCombination_surjective
linearCombination_linearCombination 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule LinearMap.instFunLike linearCombination	—	induction_linear sum_add_index zero_smul add_smul sum_apply sum_single_index sum_smul_index SemigroupAction.mul_smul smul_sum sum_fun_zero
linearCombination_linear_comp 📖	mathematical	—	linearCombination DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.comp Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule RingHomCompTriple.ids	—	lhom_ext' RingHomCompTriple.ids LinearMap.ext_ring sum_single_index zero_smul one_smul
linearCombination_mapDomain 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule LinearMap.instFunLike linearCombination mapDomain	—	LinearMap.congr_fun RingHomCompTriple.ids linearCombination_comp_lmapDomain
linearCombination_onFinset 📖	mathematical	Finset Finset.instMembership	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule LinearMap.instFunLike linearCombination onFinset Finset.sum SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Finset.sum_congr support_onFinset Finset.sum_filter_of_ne Mathlib.Tactic.Contrapose.contrapose₄ zero_smul
linearCombination_option 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule LinearMap.instFunLike linearCombination AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instFunLike some	—	linearCombination_apply sum_option_index_smul
linearCombination_range 📖	mathematical	—	LinearMap.range Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule RingHom.id RingHomSurjective.ids linearCombination Top.top Submodule Submodule.instTop	—	RingHomSurjective.ids LinearMap.range_eq_top linearCombination_surjective
linearCombination_restrict 📖	mathematical	—	linearCombination Set.Elem Set.restrict LinearMap.comp Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Submodule SetLike.instMembership Submodule.setLike Submodule.span Set.image instAddCommMonoid Submodule.addCommMonoid module Semiring.toModule Submodule.module RingHom.id RingHomCompTriple.ids Submodule.subtype supported linearCombinationOn LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm supportedEquivFinsupp	—	lhom_ext' RingHomCompTriple.ids RingHomInvPair.ids LinearMap.ext_ring linearCombination_single one_smul LinearMap.comp.congr_simp LinearMap.comp_codRestrict LinearMap.subtype_comp_codRestrict supportedEquivFinsupp_symm_apply_coe extendDomain_single
linearCombination_single 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule LinearMap.instFunLike linearCombination single SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	sum_single_index zero_smul
linearCombination_single_index 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule LinearMap.instFunLike linearCombination Pi.single AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instFunLike	—	linearCombination_apply sum_eq_single Pi.single_eq_of_ne smul_zero zero_smul Pi.single_eq_same
linearCombination_smul 📖	mathematical	—	linearCombination SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction LinearMap.comp Finsupp NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass instAddCommMonoid module Semiring.toModule RingHom.id RingHomCompTriple.ids LinearMap.restrictScalars LinearMap.CompatibleSMul.finsupp_dom AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne LinearMap.IsScalarTower.compatibleSMul' mapRange.linearMap LinearEquiv.toLinearMap RingHomInvPair.ids instZero curryLinearEquiv	—	lhom_ext' RingHomCompTriple.ids LinearMap.CompatibleSMul.finsupp_dom LinearMap.IsScalarTower.compatibleSMul' RingHomInvPair.ids LinearMap.ext_ring linearCombination_single one_smul curry_single LinearMap.map_zero mapRange_single
linearCombination_surjective 📖	mathematical	—	Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe LinearMap RingHom.id instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule LinearMap.instFunLike linearCombination	—	linearCombination_single one_smul
linearCombination_unique 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule LinearMap.instFunLike linearCombination SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instFunLike Unique.instInhabited	—	linearCombination_single unique_single
linearCombination_zero 📖	mathematical	—	linearCombination Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid LinearMap RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule LinearMap.instZero	—	LinearMap.ext linearCombination_zero_apply
linearCombination_zero_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule LinearMap.instFunLike linearCombination Pi.instZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	smul_zero sum_fun_zero
lmapDomain_linearCombination 📖	mathematical	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	LinearMap.comp Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass instAddCommMonoid module Semiring.toModule RingHomCompTriple.ids linearCombination lmapDomain	—	lhom_ext' RingHomCompTriple.ids LinearMap.ext_ring mapDomain_single sum_single_index zero_smul one_smul
mem_span_iff_linearCombination 📖	mathematical	—	Submodule SetLike.instMembership Submodule.setLike Submodule.span DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Finsupp Set.Elem MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule LinearMap.instFunLike linearCombination Set Set.instMembership	—	RingHomSurjective.ids SetLike.ext_iff span_eq_range_linearCombination
mem_span_image_iff_linearCombination 📖	mathematical	—	Submodule SetLike.instMembership Submodule.setLike Submodule.span Set.image Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instAddCommMonoid module Semiring.toModule supported DFunLike.coe LinearMap RingHom.id MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass LinearMap.instFunLike linearCombination	—	RingHomSurjective.ids span_image_eq_map_linearCombination
mem_span_range_iff_exists_finsupp 📖	mathematical	—	Submodule SetLike.instMembership Submodule.setLike Submodule.span Set.range sum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	RingHomSurjective.ids
range_linearCombination 📖	mathematical	—	LinearMap.range Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule RingHom.id RingHomSurjective.ids linearCombination Submodule.span Set.range	—	Submodule.ext RingHomSurjective.ids LinearMap.mem_range linearCombination_apply sum_mem Submodule.addSubmonoidClass Submodule.smul_mem Submodule.subset_span Set.mem_range_self Submodule.span_le SetLike.mem_coe linearCombination_single one_smul
span_eq_range_linearCombination 📖	mathematical	—	Submodule.span LinearMap.range Finsupp Set Set.instMembership MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule RingHom.id RingHomSurjective.ids linearCombination	—	RingHomSurjective.ids range_linearCombination Subtype.range_coe_subtype Set.setOf_mem_eq
span_image_eq_map_linearCombination 📖	mathematical	—	Submodule.span Set.image Submodule.map Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule RingHom.id RingHomSurjective.ids linearCombination supported	—	Submodule.span_eq_of_le RingHomSurjective.ids Set.mem_image single_mem_supported linearCombination_single one_smul Submodule.map_le_iff_le_comap Submodule.smul_mem Submodule.subset_span Set.mem_image_of_mem mem_supported' zero_smul AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass Submodule.mem_comap linearCombination_apply sum_mem

Fintype

Definitions

Name	Category	Theorems
bilinearCombination 📖	CompOp	2 math math: bilinearCombination_apply_single, bilinearCombination_apply
linearCombination 📖	CompOp	17 math math: IsBaseChange.of_fintype_basis_eq, PiToModule.fromEnd_apply, bilinearCombination_apply, RootPairing.EmbeddedG2.allRoots_eq_map_allCoeffs, Matrix.GeneralLinearGroup.toLin'_apply, IsBaseChange.of_fintype_basis, span_range_eq_top_iff_surjective_fintypeLinearCombination, range_linearCombination, Matrix.represents_iff, Matrix.Represents.congr_fun, LinearIndependent.fintypeLinearCombination_injective, linearIndependent_iff_injective_fintypeLinearCombination, PiToModule.fromMatrix_apply, Finsupp.linearCombination_eq_fintype_linearCombination, linearCombination_apply_single, linearCombination_apply, Finsupp.linearCombination_eq_fintype_linearCombination_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bilinearCombination_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.addCommMonoid LinearMap.module LinearMap.instFunLike bilinearCombination linearCombination	—	—
bilinearCombination_apply_single 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module bilinearCombination Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	linearCombination_apply_single
linearCombination_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike linearCombination Finset.sum Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—
linearCombination_apply_single 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike linearCombination Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Finset.sum_congr Pi.single_apply ite_smul zero_smul Finset.sum_ite_eq' Finset.mem_univ
mem_span_image_iff_exists_fun 📖	mathematical	—	Submodule SetLike.instMembership Submodule.setLike Submodule.span Set.image Finset.sum Set.Elem Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set Set.instMembership	—	Submodule.mem_span_range_iff_exists_fun Set.image_eq_range
range_linearCombination 📖	mathematical	—	LinearMap.range Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule RingHom.id RingHomSurjective.ids linearCombination Submodule.span Set.range	—	RingHomSurjective.ids RingHomCompTriple.ids RingHomInvPair.ids Finite.of_fintype Finsupp.linearCombination_eq_fintype_linearCombination LinearMap.range_comp RingHomSurjective.invPair LinearEquiv.range Submodule.map_top Finsupp.range_linearCombination

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_finsupp_linearCombination 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule Finsupp.linearCombination	—	Finsupp.apply_linearCombination

Span

Definitions

Name	Category	Theorems
repr 📖	CompOp	3 math math: repr_def, LinearIndependent.span_repr_eq, finsupp_linearCombination_repr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finsupp_linearCombination_repr 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Finsupp Set Set.instMembership MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike Finsupp.linearCombination repr Submodule SetLike.instMembership Submodule.setLike Submodule.span	—	repr_def Finsupp.mem_span_iff_linearCombination
repr_def 📖	mathematical	—	repr Finsupp Set.Elem MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe LinearMap RingHom.id Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike Finsupp.linearCombination Set Set.instMembership Submodule SetLike.instMembership Submodule.setLike Submodule.span	—	—

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_span_finset 📖	mathematical	—	Submodule SetLike.instMembership setLike span SetLike.coe Finset Finset.instSetLike Set Set.instHasSubset Function.support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finset.sum SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	mem_span_iff_exists_finset_subset HasSubset.Subset.trans Set.instIsTransSubset Finset.sum_subset Function.support_subset_iff' zero_smul sum_mem addSubmonoidClass smul_mem subset_span
mem_span_finset' 📖	mathematical	—	Submodule SetLike.instMembership setLike span SetLike.coe Finset Finset.instSetLike Finset.sum Finset.univ Finset.Subtype.fintype SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	mem_span_iff_of_fintype
mem_span_iff_exists_finset_subset 📖	mathematical	—	Submodule SetLike.instMembership setLike span Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike Function.support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finset.sum SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Set.image_id Finsupp.mem_span_image_iff_linearCombination Set.image_congr Set.image_id' Finsupp.fun_support_eq Set.instReflSubset Finset.sum_congr sum_mem addSubmonoidClass smul_mem subset_span
mem_span_iff_of_fintype 📖	mathematical	—	Submodule SetLike.instMembership setLike span Finset.sum Set.Elem Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set Set.instMembership	—	Subtype.range_val mem_span_range_iff_exists_fun
mem_span_image_iff_exists_fun 📖	mathematical	—	Submodule SetLike.instMembership setLike span Set.image Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike Finset.sum Finset.univ Finset.Subtype.fintype SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Finsupp.mem_span_image_iff_linearCombination Finset.sum_coe_sort sum_smul_mem subset_span
mem_span_range_iff_exists_fun 📖	mathematical	—	Submodule SetLike.instMembership setLike span Set.range Finset.sum Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Finite.of_fintype Function.Surjective.exists Equiv.surjective Finset.sum_congr Finsupp.sum_fintype zero_smul
mem_span_set 📖	mathematical	—	Submodule SetLike.instMembership setLike span Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike Finsupp.support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.sum SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Set.image_id Finsupp.mem_span_image_iff_linearCombination
mem_span_set' 📖	mathematical	—	Submodule SetLike.instMembership setLike span Finset.sum Finset.univ Fin.fintype SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set Set.instMembership	—	mem_span_set Finsupp.sum.eq_1 Finset.sum_coe_sort Fintype.sum_equiv sum_mem smul_mem subset_span
span_eq_iUnion_nat 📖	mathematical	—	SetLike.coe Submodule setLike span Set.iUnion Set.image Finset.sum Finset.univ Fin.fintype SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction setOf	—	Set.ext
top_le_span_range_iff_forall_exists_fun 📖	mathematical	—	Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder Top.top instTop span Set.range Finset.sum Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
span_range_eq_top_iff_surjective_finsuppLinearCombination 📖	mathematical	—	Submodule.span Set.range Top.top Submodule Submodule.instTop Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe LinearMap RingHom.id Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike Finsupp.linearCombination	—	RingHomSurjective.ids LinearMap.range_eq_top Finsupp.range_linearCombination
span_range_eq_top_iff_surjective_fintypeLinearCombination 📖	mathematical	—	Submodule.span Set.range Top.top Submodule Submodule.instTop DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike Fintype.linearCombination	—	RingHomSurjective.ids LinearMap.range_eq_top Fintype.range_linearCombination

---

← Back to Index