Span

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

Statistics

Metric	Count
Definitions	0
Theorems disjoint_lsingle_lsingle, iInf_ker_lapply_le_bot, iSup_lsingle_range, ker_lsingle, lsingle_range_le_ker_lapply, range_lmapDomain, span_single_eq_top, span_single_image, exists_finset_of_mem_iSup, image_smul_top_eq_range_lsum, mem_iSup_iff_exists_finset, mem_sSup_iff_exists_finset, range_lsum_smul, smul_top_eq_range_lsum	14
Total	14

Finsupp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disjoint_lsingle_lsingle 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	Disjoint Submodule Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module Submodule.instPartialOrder Submodule.instOrderBot iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Set Set.instMembership LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids lsingle	—	Disjoint.mono RingHomSurjective.ids lsingle_range_le_ker_lapply disjoint_compl_right disjoint_iff_inf_le le_trans le_iInf Disjoint.le_bot inf_le_of_right_le iInf_le_of_le iInf_le inf_le_of_left_le iInf_ker_lapply_le_bot
iInf_ker_lapply_le_bot 📖	mathematical	—	Submodule Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder iInf Submodule.instInfSet LinearMap.ker RingHom.id Semiring.toNonAssocSemiring lapply Bot.bot Submodule.instBot	—	instIsConcreteLE ext
iSup_lsingle_range 📖	mathematical	—	iSup Submodule Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids lsingle Top.top Submodule.instTop	—	RingHomSurjective.ids eq_top_iff SetLike.le_def instIsConcreteLE sum_single sum_mem Submodule.addSubmonoidClass Submodule.mem_iSup_of_mem
ker_lsingle 📖	mathematical	—	LinearMap.ker Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module RingHom.id Semiring.toNonAssocSemiring lsingle Bot.bot Submodule Submodule.instBot	—	LinearMap.ker_eq_bot_of_injective single_injective
lsingle_range_le_ker_lapply 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	Submodule Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Set Set.instMembership LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids lsingle iInf Submodule.instInfSet LinearMap.ker lapply	—	iSup_le RingHomSurjective.ids LinearMap.range_le_iff_comap RingHomCompTriple.ids Submodule.comap_iInf iInf_congr_Prop LinearMap.ker_comp instIsConcreteLE Disjoint.le_bot single_eq_of_ne
range_lmapDomain 📖	mathematical	—	LinearMap.range Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instAddCommMonoid module Semiring.toModule RingHom.id RingHomSurjective.ids lmapDomain Submodule.span Set.range single AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	le_antisymm RingHomSurjective.ids induction_linear mapDomain_zero AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass Submodule.add_mem lmapDomain_apply mapDomain_single smul_single_one Submodule.smul_mem Submodule.subset_span Submodule.span_le Set.range_subset_iff
span_single_eq_top 📖	mathematical	—	Submodule.span Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module setOf single Top.top Submodule Submodule.instTop	—	Submodule.eq_top_iff' induction_linear Submodule.zero_mem AddMemClass.add_mem AddSubmonoidClass.toAddMemClass Submodule.addSubmonoidClass Submodule.mem_span_of_mem
span_single_image 📖	mathematical	—	Submodule.span Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module Set.image single Submodule.map RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids lsingle	—	RingHomSurjective.ids Submodule.span_image

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_finset_of_mem_iSup 📖	mathematical	Submodule SetLike.instMembership setLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice	Finset Submodule SetLike.instMembership setLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice Finset.instSetLike	—	CompleteLattice.IsCompactElement.exists_finset_of_le_iSup singleton_span_isCompactElement
image_smul_top_eq_range_lsum 📖	mathematical	—	Set Submodule CommSemiring.toSemiring pointwiseSetSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.image Top.top instTop LinearMap.range Finsupp Set.Elem AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids DFunLike.coe LinearEquiv RingHomInvPair.ids LinearMap Pi.addCommMonoid LinearMap.addCommMonoid Pi.Function.module LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid EquivLike.toFunLike LinearEquiv.instEquivLike Finsupp.lsum LinearMap.instSMul DistribMulAction.toDistribSMul Set.instMembership LinearMap.id	—	RingHomSurjective.ids RingHomInvPair.ids smulCommClass_self Set.range_comp Subtype.range_coe_subtype LinearMap.range_id range_lsum_smul
mem_iSup_iff_exists_finset 📖	mathematical	—	Submodule SetLike.instMembership setLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice Finset Finset.instSetLike	—	exists_finset_of_mem_iSup iSup_mono iSup_const_le
mem_sSup_iff_exists_finset 📖	mathematical	—	Submodule SetLike.instMembership setLike SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice Finset Set Set.instHasSubset SetLike.coe Finset.instSetLike iSup	—	sSup_eq_iSup iSup_subtype' mem_iSup_iff_exists_finset Finset.coe_map Set.image_congr Subtype.coe_preimage_self iSup_congr_Prop iSup_exists Function.Injective.injOn Subtype.coe_injective iSup_subtype iSup_and'
range_lsum_smul 📖	mathematical	—	LinearMap.range Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid CommSemiring.toSemiring Finsupp.instAddCommMonoid Finsupp.module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids DFunLike.coe LinearEquiv RingHomInvPair.ids LinearMap Pi.addCommMonoid LinearMap.addCommMonoid Pi.Function.module LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Module.toDistribMulAction EquivLike.toFunLike LinearEquiv.instEquivLike Finsupp.lsum LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Set Submodule pointwiseSetSMul Set.range	—	RingHomSurjective.ids RingHomInvPair.ids smulCommClass_self LinearMap.range_eq_map map.congr_simp map_span set_smul_span Set.image_congr Set.image_univ Set.ext Finsupp.sum_single_index map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass smul_zero
smul_top_eq_range_lsum 📖	mathematical	—	Set Submodule CommSemiring.toSemiring pointwiseSetSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Top.top instTop LinearMap.range Finsupp Set.Elem AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids DFunLike.coe LinearEquiv RingHomInvPair.ids LinearMap Pi.addCommMonoid LinearMap.addCommMonoid Pi.Function.module LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid EquivLike.toFunLike LinearEquiv.instEquivLike Finsupp.lsum LinearMap.instSMul DistribMulAction.toDistribSMul Set.instMembership LinearMap.id	—	RingHomSurjective.ids RingHomInvPair.ids smulCommClass_self Set.image_congr Set.image_id' image_smul_top_eq_range_lsum

---

← Back to Index