Basic

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

Statistics

Metric	Count
Definitions `coord`, `toSpanNonzeroSingleton`, `toSpanSingleton`, `inclusionSpan`, `prod`	5
Theorems `toIntSubmodule_closure`, `toNatSubmodule_closure`, `coord_apply_smul`, `coord_self`, `toSpanNonzeroSingleton_apply`, `toSpanNonzeroSingleton_one`, `toSpanNonzeroSingleton_symm_apply_smul`, `apply_apply_mem_of_mem_span`, `comp_toSpanSingleton`, `eqOn_span`, `eqOn_span'`, `eqOn_span_iff`, `exists_ne_zero_of_sSup_eq`, `ext_on`, `ext_on_range`, `isIdempotentElem_apply_one_iff`, `isIdempotentElem_map_one_iff`, `ker_inf_lt_ker_inf_of_map_eq_of_lt`, `ker_toSpanSingleton`, `ker_toSpanSingleton_eq_bot_iff`, `map_eq_top_iff`, `map_injective`, `map_le_map_iff`, `map_le_map_iff'`, `map_span`, `map_span_le`, `range_domRestrict_eq_range_iff`, `range_toSpanSingleton`, `smulRight_id`, `span_preimage_le`, `span_singleton_eq_range`, `span_singleton_sup_ker_eq_top`, `submoduleOf_span_singleton_of_mem`, `surjective_domRestrict_iff`, `toSpanSingleton_add`, `toSpanSingleton_apply`, `toSpanSingleton_apply_one`, `toSpanSingleton_eq_zero_iff`, `toSpanSingleton_injective`, `toSpanSingleton_isIdempotentElem_iff`, `toSpanSingleton_one`, `toSpanSingleton_smul`, `toSpanSingleton_zero`, `submoduleSpan`, `apply_mem_span_image_iff_mem_span`, `apply_mem_span_image_of_mem_span`, `biSup_comap_eq_top_of_range_eq_biSup`, `biSup_comap_eq_top_of_surjective`, `biSup_comap_subtype_eq_top`, `coe_scott_continuous`, `comap_covBy_of_surjective`, `comap_le_comap_iff_of_le_range`, `comap_map_eq`, `comap_map_eq_self`, `comap_map_sup_of_comap_le`, `comap_sup_of_injective`, `covBy_span_singleton_sup`, `disjoint_span_singleton`, `disjoint_span_singleton'`, `disjoint_span_singleton''`, `disjoint_span_singleton_of_notMem`, `finite_span_isCompactElement`, `finset_span_isCompactElement`, `iSup_induction`, `iSup_induction'`, `iSup_toAddSubmonoid`, `image_span_subset`, `image_span_subset_span`, `inclusionSpan_apply_coe`, `injective_inclusionSpan`, `instIsCompactlyGenerated`, `instIsModularLattice`, `isCoatom_comap_iff`, `isCoatom_comap_or_eq_top`, `isCoatom_map_of_ker_le`, `isCompl_comap_subtype_of_isCompl_of_le`, `isCompl_span_singleton_of_isCoatom_of_notMem`, `linearMap_eq_iff_of_eq_span`, `linearMap_eq_iff_of_span_eq_top`, `linearMap_eq_zero_iff_of_eq_span`, `linearMap_eq_zero_iff_of_span_eq_top`, `map_iInf_of_ker_le`, `map_lt_map_of_le_of_sup_lt_sup`, `map_span`, `map_span_le`, `map_strict_mono_of_ker_inf_eq`, `map_strict_mono_or_ker_sup_lt_ker_sup`, `map_subtype_span_singleton`, `mapsTo_span`, `mem_prod`, `notMem_span_of_apply_notMem_span_image`, `prod_bot`, `prod_coe`, `prod_inf_prod`, `prod_mono`, `prod_sup_prod`, `prod_top`, `singleton_span_isCompactElement`, `span_coe_eq_restrictScalars`, `span_eq_top_of_span_eq_top`, `span_image`, `span_image_linearEquiv`, `span_le_restrictScalars`, `span_neg`, `span_preimage_le`, `span_prod_le`, `span_range_inclusionSpan`, `span_range_inclusion_eq_top`, `span_range_inclusion_restrictScalars_eq_top`, `span_range_subtype_eq_top_iff`, `span_singleton_eq_span_singleton`, `span_smul_eq_of_isUnit`, `span_span_of_tower`, `span_subset_span`, `wcovBy_span_singleton_sup`	115
Total	120

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toIntSubmodule_closure` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `AddSubgroup` `AddCommGroup.toAddGroup` `Submodule` `Int.instSemiring` `AddCommGroup.toAddCommMonoid` `AddCommGroup.toIntModule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Submodule.instPartialOrder` `instFunLikeOrderIso` `toIntSubmodule` `closure` `Submodule.span`	—	`LE.le.antisymm'` `Submodule.span_le` `subset_closure` `closure_le` `Submodule.subset_span`

AddSubmonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toNatSubmodule_closure` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Submodule` `Nat.instSemiring` `AddCommMonoid.toNatModule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Submodule.instPartialOrder` `instFunLikeOrderIso` `toNatSubmodule` `closure` `Submodule.span`	—	`LE.le.antisymm'` `Submodule.span_le` `subset_closure` `closure_le` `Submodule.subset_span`

LinearEquiv

Definitions

Name	Category	Theorems
`coord` 📖	CompOp	2 math math: `coord_self`, `coord_apply_smul`
`toSpanNonzeroSingleton` 📖	CompOp	4 math math: `toSpanNonzeroSingleton_homothety`, `toSpanNonzeroSingleton_apply`, `toSpanNonzeroSingleton_symm_apply_smul`, `toSpanNonzeroSingleton_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coord_apply_smul` 📖	mathematical	—	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set` `Set.instSingletonSet` `Submodule.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Submodule.module` `Semiring.toModule` `EquivLike.toFunLike` `instEquivLike` `coord`	—	`RingHomInvPair.ids` `apply_symm_apply`
`coord_self` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set` `Set.instSingletonSet` `Submodule.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Submodule.module` `Semiring.toModule` `EquivLike.toFunLike` `instEquivLike` `coord` `Submodule.mem_span_singleton_self` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`RingHomInvPair.ids` `Submodule.mem_span_singleton_self` `toSpanNonzeroSingleton_one` `symm_apply_apply`
`toSpanNonzeroSingleton_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set` `Set.instSingletonSet` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Submodule.addCommMonoid` `Semiring.toModule` `Submodule.module` `EquivLike.toFunLike` `instEquivLike` `toSpanNonzeroSingleton` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Submodule.smul_mem` `Submodule.mem_span_singleton_self`	—	`RingHomInvPair.ids`
`toSpanNonzeroSingleton_one` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set` `Set.instSingletonSet` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Submodule.addCommMonoid` `Semiring.toModule` `Submodule.module` `EquivLike.toFunLike` `instEquivLike` `toSpanNonzeroSingleton` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Submodule.mem_span_singleton_self`	—	`RingHomInvPair.ids` `Submodule.mem_span_singleton_self` `Submodule.smul_mem` `one_smul` `toSpanNonzeroSingleton_apply`
`toSpanNonzeroSingleton_symm_apply_smul` 📖	mathematical	—	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set` `Set.instSingletonSet` `Submodule.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Submodule.module` `Semiring.toModule` `EquivLike.toFunLike` `instEquivLike` `symm` `toSpanNonzeroSingleton`	—	`RingHomInvPair.ids` `apply_symm_apply`

LinearMap

Definitions

Name	Category	Theorems
`toSpanSingleton` 📖	CompOp	40 math math: `comp_toSpanSingleton`, `adjoint_innerₛₗ_apply`, `intrinsicStar_toSpanSingleton`, `smulRight_id`, `IsIdempotentElem.ker_toSpanSingleton_eq_span`, `IsSimpleModule.toSpanSingleton_surjective`, `toSpanSingleton_one_eq_algebraLinearMap`, `ker_toSpanSingleton`, `lsmul_flip_apply`, `toSpanSingleton_apply_one`, `CharacterModule.intSpanEquivQuotAddOrderOf_symm_apply_coe`, `range_toSpanSingleton`, `CharacterModule.intSpanEquivQuotAddOrderOf_apply`, `ker_toSpanSingleton_eq_bot_iff`, `toSpanSingleton_smul`, `IsIdempotentElem.ker_toSpanSingleton_one_sub_eq_span`, `ContinuousLinearMap.toLinearMap_toSpanSingleton`, `adjoint_toSpanSingleton`, `ContinuousLinearEquiv.toSpanNonzeroSingleton_symm_apply`, `toSpanSingleton_apply`, `Submodule.annihilator_span_singleton`, `toSpanSingleton_eq_zero_iff`, `LinearIsometry.coe_toSpanSingleton`, `toSpanSingleton_homothety`, `toSpanSingleton_eq_algebra_linearMap`, `Submodule.annihilator_span`, `toSpanSingleton_convMul_toSpanSingleton`, `toMatrix_toSpanSingleton`, `Ideal.coe_torsionOf`, `toSpanSingleton_zero`, `toSpanSingleton_one`, `isSimpleModule_iff_toSpanSingleton_surjective`, `DualNumber.algHom_ext'_iff`, `Module.exists_ker_toSpanSingleton_eq_annihilator`, `span_singleton_eq_range`, `toSpanSingleton_injective`, `toSpanSingleton_isIdempotentElem_iff`, `IsSimpleModule.ker_toSpanSingleton_isMaximal`, `lsum_comp_mapRange_toSpanSingleton`, `toSpanSingleton_add`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_toSpanSingleton` 📖	mathematical	—	`comp` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `RingHomCompTriple.ids` `toSpanSingleton` `DFunLike.coe` `LinearMap` `instFunLike`	—	`ext_ring` `RingHomCompTriple.ids` `one_smul`
`eqOn_span` 📖	—	`Set.EqOn` `DFunLike.coe` `LinearMap` `instFunLike` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span`	—	—	`eqOn_span'`
`eqOn_span'` 📖	mathematical	`Set.EqOn` `DFunLike.coe` `LinearMap` `instFunLike`	`SetLike.coe` `Submodule` `Submodule.setLike` `Submodule.span`	—	`eqOn_span_iff`
`eqOn_span_iff` 📖	mathematical	—	`Set.EqOn` `DFunLike.coe` `LinearMap` `instFunLike` `SetLike.coe` `Submodule` `Submodule.setLike` `Submodule.span`	—	`semilinearMapClass` `le_eqLocus` `Submodule.span_le`
`exists_ne_zero_of_sSup_eq` 📖	—	`SupSet.sSup` `Submodule` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice`	—	—	`RingHomCompTriple.ids` `LE.le.trans_eq` `le_sSup` `exists_ne_zero_of_sSup_eq_top` `sSup_image` `sSup_eq_iSup` `Submodule.biSup_comap_subtype_eq_top` `ext`
`ext_on` 📖	—	`Submodule.span` `Top.top` `Submodule` `Submodule.instTop` `Set.EqOn` `DFunLike.coe` `LinearMap` `instFunLike`	—	—	`DFunLike.ext` `eqOn_span` `Submodule.eq_top_iff'`
`ext_on_range` 📖	—	`Submodule.span` `Set.range` `Top.top` `Submodule` `Submodule.instTop` `DFunLike.coe` `LinearMap` `instFunLike`	—	—	`ext_on` `Set.forall_mem_range`
`isIdempotentElem_apply_one_iff` 📖	mathematical	—	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `Module.End` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule` `instFunLike` `RingHom.id` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Module.End.instMul`	—	`isIdempotentElem_map_one_iff`
`isIdempotentElem_map_one_iff` 📖	mathematical	—	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `Module.End` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule` `instFunLike` `RingHom.id` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Module.End.instMul`	—	`IsIdempotentElem.eq_1` `smul_eq_mul` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `semilinearMapClass` `mul_one` `ext_iff`
`ker_inf_lt_ker_inf_of_map_eq_of_lt` 📖	mathematical	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.map`	`Submodule.instMin` `ker`	—	`Submodule.map_strict_mono_or_ker_sup_lt_ker_sup` `Eq.not_lt`
`ker_toSpanSingleton` 📖	mathematical	—	`ker` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `toSpanSingleton` `Bot.bot` `Submodule` `Submodule.instBot`	—	`SetLike.ext` `smul_eq_zero` `IsDomain.toIsCancelMulZero`
`ker_toSpanSingleton_eq_bot_iff` 📖	mathematical	—	`ker` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `toSpanSingleton` `Bot.bot` `Submodule` `Submodule.instBot` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisorsRight`	—	`le_bot_iff`
`map_eq_top_iff` 📖	mathematical	`range` `AddCommGroup.toAddCommMonoid` `Top.top` `Submodule` `Submodule.instTop`	`Submodule.map` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `ker`	—	`range_eq_map`
`map_injective` 📖	mathematical	`ker` `AddCommGroup.toAddCommMonoid` `Bot.bot` `Submodule` `Submodule.instBot`	`Submodule.map`	—	`le_antisymm` `map_le_map_iff'` `le_of_eq` `ge_of_eq`
`map_le_map_iff` 📖	mathematical	—	`Submodule` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.map` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `ker`	—	`Submodule.map_le_iff_le_comap` `Submodule.comap_map_eq`
`map_le_map_iff'` 📖	mathematical	`ker` `AddCommGroup.toAddCommMonoid` `Bot.bot` `Submodule` `Submodule.instBot`	`Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.map`	—	`map_le_map_iff` `sup_bot_eq`
`map_span` 📖	mathematical	—	`Submodule.map` `Submodule.span` `Set.image` `DFunLike.coe` `LinearMap` `instFunLike`	—	`Submodule.map_span`
`map_span_le` 📖	mathematical	—	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.map` `Submodule.span` `SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `LinearMap` `instFunLike`	—	`Submodule.map_span_le`
`range_domRestrict_eq_range_iff` 📖	mathematical	—	`range` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `domRestrict` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `ker` `Top.top` `Submodule.instTop`	—	`eq_top_iff` `mem_range_self` `Submodule.add_mem_sup` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass` `sub_self` `add_sub_cancel` `le_antisymm` `range_domRestrict_le_range` `Submodule.mem_sup` `map_add` `SemilinearMapClass.toAddHomClass` `mem_ker` `add_zero`
`range_toSpanSingleton` 📖	mathematical	—	`range` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `RingHomSurjective.ids` `toSpanSingleton` `Submodule.span` `Set` `Set.instSingletonSet`	—	`SetLike.coe_injective` `RingHomSurjective.ids` `Submodule.span_singleton_eq_range`
`smulRight_id` 📖	mathematical	—	`smulRight` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `id` `toSpanSingleton`	—	`IsScalarTower.left`
`span_preimage_le` 📖	mathematical	—	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.span` `Set.preimage` `DFunLike.coe` `LinearMap` `instFunLike` `Submodule.comap`	—	`Submodule.span_preimage_le`
`span_singleton_eq_range` 📖	mathematical	—	`Submodule.span` `Set` `Set.instSingletonSet` `range` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `RingHomSurjective.ids` `toSpanSingleton`	—	`RingHomSurjective.ids` `range_toSpanSingleton`
`span_singleton_sup_ker_eq_top` 📖	mathematical	—	`Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Submodule.span` `Set` `Set.instSingletonSet` `ker` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Semiring.toModule` `RingHom.id` `Semiring.toNonAssocSemiring` `Top.top` `Submodule.instTop`	—	`top_unique` `Submodule.mem_sup` `Submodule.mem_span_singleton` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `inv_mul_cancel_right₀` `sub_self` `add_sub_cancel`
`submoduleOf_span_singleton_of_mem` 📖	mathematical	`Submodule` `SetLike.instMembership` `Submodule.setLike`	`Submodule.submoduleOf` `Submodule.span` `Set` `Set.instSingletonSet` `Submodule.addCommMonoid` `Submodule.module`	—	`Submodule.ext` `SMulMemClass.smul_mem` `Submodule.smulMemClass`
`surjective_domRestrict_iff` 📖	mathematical	`DFunLike.coe` `LinearMap` `AddCommGroup.toAddCommMonoid` `instFunLike`	`Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `domRestrict` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `ker` `Top.top` `Submodule.instTop`	—	`range_eq_top` `range_domRestrict_eq_range_iff`
`toSpanSingleton_add` 📖	mathematical	—	`toSpanSingleton` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `instAdd`	—	`ext_ring` `smul_add` `one_smul`
`toSpanSingleton_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `instFunLike` `toSpanSingleton` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—
`toSpanSingleton_apply_one` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `instFunLike` `toSpanSingleton` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`one_smul`
`toSpanSingleton_eq_zero_iff` 📖	mathematical	—	`toSpanSingleton` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`toSpanSingleton_zero` `toSpanSingleton_injective`
`toSpanSingleton_injective` 📖	mathematical	—	`LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `toSpanSingleton`	—	`one_smul`
`toSpanSingleton_isIdempotentElem_iff` 📖	mathematical	—	`IsIdempotentElem` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Module.End.instMul` `toSpanSingleton` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_assoc` `one_mul`
`toSpanSingleton_one` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `instFunLike` `toSpanSingleton` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`toSpanSingleton_apply_one`
`toSpanSingleton_smul` 📖	mathematical	—	`toSpanSingleton` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `instSMul`	—	`ext_ring` `one_smul`
`toSpanSingleton_zero` 📖	mathematical	—	`toSpanSingleton` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `instZero`	—	`ext_ring` `smul_zero`

LinearMap.BilinMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_apply_mem_of_mem_span` 📖	—	`Submodule` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Submodule.span`	—	—	`smulCommClass_self` `Submodule.span_induction₂` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `map_add` `SemilinearMapClass.toAddHomClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `Submodule.smul_mem`

Set.MapsTo

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`submoduleSpan` 📖	mathematical	`Set.MapsTo` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	`SetLike.coe` `Submodule` `Submodule.setLike` `Submodule.span`	—	`Submodule.mapsTo_span`

Submodule

Definitions

Name	Category	Theorems
`inclusionSpan` 📖	CompOp	3 math math: `injective_inclusionSpan`, `inclusionSpan_apply_coe`, `span_range_inclusionSpan`
`prod` 📖	CompOp	44 math math: `prod_inf_prod`, `LinearMap.prod_eq_inf_comap`, `LinearMap.range_prodMap`, `LinearMap.ker_coprod_of_disjoint_range`, `FG.prod`, `comap_fst`, `prod_coe`, `mem_prod`, `prod_mono`, `prod_comap_inr`, `LinearMap.prodMap_comap_prod`, `prod_le_iff`, `LinearMap.span_inl_union_inr`, `LinearMap.map_coprod_prod`, `LinearMap.ker_prodMap`, `prod_top`, `span_prod_le`, `LinearMap.ker_prod_ker_le_ker_coprod`, `prod_eq_bot_iff`, `LinearPMap.snd_apply`, `comap_snd`, `LinearMap.range_prod_eq`, `LinearPMap.fst_apply`, `prod_eq_top_iff`, `map_inr`, `goursatFst_prod_goursatSnd_le`, `LinearMap.range_prod_le`, `LinearMap.prodMap_map_prod`, `map_inl`, `prod_comap_inl`, `ContinuousLinearMap.range_eq_map_coprodSubtypeLEquivOfIsCompl`, `prod_bot`, `LinearMap.comap_prod_prod`, `ContinuousLinearMap.ker_prod_ker_le_ker_coprod`, `LinearMap.coprod_map_prod`, `ContinuousLinearMap.range_prod_eq`, `prod_map_fst`, `ContinuousLinearMap.ker_coprod_of_disjoint_range`, `le_prod_iff`, `Subalgebra.prod_toSubmodule`, `NonUnitalSubalgebra.prod_toSubmodule`, `prod_sup_prod`, `LinearMap.prod_eq_sup_map`, `prod_map_snd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_mem_span_image_iff_mem_span` 📖	mathematical	`DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	`Submodule` `SetLike.instMembership` `setLike` `span` `Set.image`	—	`mem_comap` `map_span` `comap_map_eq_of_injective`
`apply_mem_span_image_of_mem_span` 📖	mathematical	`Submodule` `SetLike.instMembership` `setLike` `span`	`Set.image` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	—	`span_image` `mem_map_of_mem`
`biSup_comap_eq_top_of_range_eq_biSup` 📖	mathematical	`Set.Nonempty` `LinearMap.range` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `iSup` `Submodule` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `Set` `Set.instMembership`	`comap` `Top.top` `instTop`	—	`biSup_comap_subtype_eq_top` `biSup_comap_eq_top_of_surjective` `LinearMap.surjective_rangeRestrict`
`biSup_comap_eq_top_of_surjective` 📖	mathematical	`Set.Nonempty` `iSup` `Submodule` `AddCommGroup.toAddCommMonoid` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `Set` `Set.instMembership` `Top.top` `instTop` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	`comap`	—	`iSup_subtype'` `comap_map_eq` `map_iSup_comap_of_surjective` `comap_top` `left_eq_sup` `le_trans` `LinearMap.ker_le_comap` `le_biSup`
`biSup_comap_subtype_eq_top` 📖	mathematical	—	`iSup` `Submodule` `SetLike.instMembership` `setLike` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `Set` `Set.instMembership` `addCommMonoid` `module` `comap` `RingHom.id` `Semiring.toNonAssocSemiring` `subtype` `Top.top` `instTop`	—	`eq_top_iff` `RingHomSurjective.ids` `map_comap_eq` `range_subtype` `inf_eq_right` `le_biSup` `map_iSup` `biSup_congr` `mem_map`
`coe_scott_continuous` 📖	mathematical	—	`OmegaCompletePartialOrder.ωScottContinuous` `Submodule` `Set` `CompleteLattice.instOmegaCompletePartialOrder` `completeLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `SetLike.coe` `setLike`	—	`OmegaCompletePartialOrder.ωScottContinuous.of_monotone_map_ωSup` `SetLike.coe_mono` `instIsConcreteLE` `coe_iSup_of_chain`
`comap_covBy_of_surjective` 📖	mathematical	`DFunLike.coe` `LinearMap` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `CovBy` `Submodule` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder`	`comap`	—	`lt_of_le_of_ne` `comap_mono` `LT.lt.le` `comap_injective_of_surjective` `LT.lt.ne` `lt_map_of_comap_lt_of_surjective` `comap_lt_comap_iff_of_surjective` `comap_map_eq` `sup_eq_left` `LE.le.trans` `LinearMap.ker_le_comap`
`comap_le_comap_iff_of_le_range` 📖	mathematical	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `LinearMap.range`	`comap`	—	`map_le_iff_le_comap` `map_comap_eq_of_le`
`comap_map_eq` 📖	mathematical	—	`comap` `AddCommGroup.toAddCommMonoid` `map` `Submodule` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `LinearMap.ker`	—	`le_antisymm` `mem_sup` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `sub_eq_zero` `add_sub_cancel` `sup_le` `le_comap_map` `comap_mono` `bot_le`
`comap_map_eq_self` 📖	mathematical	`Submodule` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `LinearMap.ker`	`comap` `map`	—	`comap_map_eq` `sup_of_le_left`
`comap_map_sup_of_comap_le` 📖	mathematical	`Submodule` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `comap`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `map`	—	`le_antisymm` `mem_sup` `sub_add_cancel` `add_mem` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `eq_sub_iff_add_eq` `add_comm` `map_le_iff_le_comap` `le_sup_left`
`comap_sup_of_injective` 📖	mathematical	`DFunLike.coe` `LinearMap` `LinearMap.instFunLike` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `LinearMap.range`	`comap` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice`	—	`map_injective_of_injective` `map_sup` `map_comap_eq_self`
`covBy_span_singleton_sup` 📖	mathematical	`Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike`	`CovBy` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `span` `Set` `Set.instSingletonSet`	—	`wcovBy_span_singleton_sup`
`disjoint_span_singleton` 📖	mathematical	—	`Disjoint` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `instOrderBot` `span` `Set` `Set.instSingletonSet` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`DivisionSemiring.to_moduleIsTorsionFree` `IsDomain.toIsCancelMulZero` `DivisionRing.isDomain` `forall_swap` `smul_mem_iff` `IsScalarTower.left` `one_ne_zero` `NeZero.one` `DivisionRing.toNontrivial`
`disjoint_span_singleton'` 📖	mathematical	—	`Disjoint` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `instOrderBot` `span` `Set` `Set.instSingletonSet` `SetLike.instMembership` `setLike`	—	—
`disjoint_span_singleton''` 📖	mathematical	—	`Disjoint` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `instOrderBot` `span` `Set` `Set.instSingletonSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`disjoint_comm`
`disjoint_span_singleton_of_notMem` 📖	mathematical	`Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike`	`Disjoint` `instPartialOrder` `instOrderBot` `span` `Set` `Set.instSingletonSet`	—	`instIsEmptyFalse`
`finite_span_isCompactElement` 📖	mathematical	—	`IsCompactElement` `Submodule` `instPartialOrder` `span`	—	`finset_span_isCompactElement` `Set.Finite.coe_toFinset`
`finset_span_isCompactElement` 📖	mathematical	—	`IsCompactElement` `Submodule` `instPartialOrder` `span` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`span_eq_iSup_of_singleton_spans` `iSup_congr_Prop` `Finset.sup_eq_iSup` `CompleteLattice.isCompactElement_finsetSup` `singleton_span_isCompactElement`
`iSup_induction` 📖	—	`Submodule` `SetLike.instMembership` `setLike` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—	`AddSubmonoid.iSup_induction` `iSup_toAddSubmonoid` `mem_toAddSubmonoid`
`iSup_induction'` 📖	—	`mem_iSup_of_mem` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `ZeroMemClass.zero_mem` `Submodule` `setLike` `AddSubmonoidClass.toZeroMemClass` `addSubmonoidClass` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `SetLike.instMembership`	—	—	`mem_iSup_of_mem` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `addSubmonoidClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `iSup_induction`
`iSup_toAddSubmonoid` 📖	mathematical	—	`toAddSubmonoid` `iSup` `Submodule` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddSubmonoid.instCompleteLattice`	—	`le_antisymm` `iSup_eq_span` `AddSubmonoid.iSup_eq_closure` `span_induction` `AddSubmonoid.subset_closure` `AddSubmonoid.zero_mem` `AddSubmonoid.add_mem` `AddSubmonoid.closure_induction` `Set.mem_iUnion` `smul_mem` `smul_zero` `smul_add` `iSup_le` `toAddSubmonoid_mono` `le_iSup`
`image_span_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.image` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike` `SetLike.coe` `Submodule` `setLike` `span` `SetLike.instMembership`	—	`Set.image_subset_iff` `span_le`
`image_span_subset_span` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.image` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike` `SetLike.coe` `Submodule` `setLike` `span`	—	`image_span_subset` `subset_span`
`inclusionSpan_apply_coe` 📖	mathematical	—	`Submodule` `SetLike.instMembership` `setLike` `span` `SetLike.coe` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `module` `module'` `LinearMap.instFunLike` `inclusionSpan`	—	—
`injective_inclusionSpan` 📖	mathematical	—	`Submodule` `SetLike.instMembership` `setLike` `span` `SetLike.coe` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `addCommMonoid` `module` `module'` `LinearMap.instFunLike` `inclusionSpan`	—	—
`instIsCompactlyGenerated` 📖	mathematical	—	`IsCompactlyGenerated` `Submodule` `completeLattice`	—	`Set.mem_image` `singleton_span_isCompactElement` `sSup_eq_iSup` `iSup_image` `span_eq_iSup_of_singleton_spans` `span_eq`
`instIsModularLattice` 📖	mathematical	—	`IsModularLattice` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice`	—	`mem_sup` `mem_inf` `add_sub_cancel_right` `add_comm` `sub_mem`
`isCoatom_comap_iff` 📖	mathematical	`DFunLike.coe` `LinearMap` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`IsCoatom` `Submodule` `PartialOrder.toPreorder` `instPartialOrder` `instOrderTop` `comap`	—	`comap_injective_of_surjective` `IsCoatom.eq_1` `comap_top` `comap_strictMono_of_surjective` `lt_map_of_comap_lt_of_surjective` `comap_map_eq_self` `LE.le.trans` `comap_mono` `bot_le` `LT.lt.le`
`isCoatom_comap_or_eq_top` 📖	mathematical	`IsCoatom` `Submodule` `AddCommGroup.toAddCommMonoid` `PartialOrder.toPreorder` `instPartialOrder` `instOrderTop`	`comap` `Top.top` `instTop`	—	`comap_map_sup_of_comap_le` `LT.lt.le` `LT.lt.not_ge` `comap_top`
`isCoatom_map_of_ker_le` 📖	mathematical	`DFunLike.coe` `LinearMap` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `LinearMap.ker` `IsCoatom` `instOrderTop`	`map`	—	`isCoatom_comap_iff` `comap_map_eq_self`
`isCompl_comap_subtype_of_isCompl_of_le` 📖	mathematical	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `CompleteLattice.toBoundedOrder` `completeLattice` `Preorder.toLE` `PartialOrder.toPreorder`	`SetLike.instMembership` `setLike` `addCommMonoid` `module` `comap` `RingHom.id` `Semiring.toNonAssocSemiring` `subtype`	—	`OrderIso.isCompl_iff` `map_comap_subtype` `inf_le_left` `Set.Iic.isCompl_inf_inf_of_isCompl_of_le` `instIsModularLattice`
`isCompl_span_singleton_of_isCoatom_of_notMem` 📖	mathematical	`IsCoatom` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `PartialOrder.toPreorder` `instPartialOrder` `instOrderTop` `SetLike.instMembership` `setLike`	`IsCompl` `CompleteLattice.toBoundedOrder` `completeLattice` `span` `Set` `Set.instSingletonSet`	—	`disjoint_span_singleton_of_notMem` `sup_comm` `covBy_top_iff` `covBy_span_singleton_sup`
`linearMap_eq_iff_of_eq_span` 📖	mathematical	`span`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `LinearMap.instFunLike` `Set` `Set.instMembership`	—	`span_induction` `zero_mem` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `add_mem` `LinearMap.map_add` `smul_mem` `LinearMap.map_smul` `LinearMap.ext`
`linearMap_eq_iff_of_span_eq_top` 📖	mathematical	`span` `Top.top` `Submodule` `instTop`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `Set` `Set.instMembership`	—	`RingHomCompTriple.ids` `LinearMap.ext` `DFunLike.congr_fun` `linearMap_eq_iff_of_eq_span`
`linearMap_eq_zero_iff_of_eq_span` 📖	mathematical	`span`	`LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `LinearMap.instZero` `DFunLike.coe` `LinearMap.instFunLike` `Set` `Set.instMembership` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`linearMap_eq_iff_of_eq_span`
`linearMap_eq_zero_iff_of_span_eq_top` 📖	mathematical	`span` `Top.top` `Submodule` `instTop`	`LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instZero` `DFunLike.coe` `LinearMap.instFunLike` `Set` `Set.instMembership` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`linearMap_eq_iff_of_span_eq_top`
`map_iInf_of_ker_le` 📖	mathematical	`DFunLike.coe` `LinearMap` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `LinearMap.ker` `iInf` `instInfSet`	`map`	—	`map_comap_eq_of_surjective` `comap_iInf` `map.congr_simp` `comap_map_eq_self` `le_iInf_iff`
`map_lt_map_of_le_of_sup_lt_sup` 📖	mathematical	`Submodule` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Preorder.toLT` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `LinearMap.ker`	`map`	—	`lt_of_le_of_ne` `map_mono` `LT.lt.ne`
`map_span` 📖	mathematical	—	`map` `span` `Set.image` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	—	`span_eq_of_le` `Set.image_mono` `subset_span` `image_span_subset_span`
`map_span_le` 📖	mathematical	—	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `map` `span` `SetLike.instMembership` `setLike` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	—	`image_span_subset`
`map_strict_mono_of_ker_inf_eq` 📖	mathematical	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `instMin` `LinearMap.ker`	`map`	—	`map_strict_mono_or_ker_sup_lt_ker_sup` `Eq.not_lt`
`map_strict_mono_or_ker_sup_lt_ker_sup` 📖	mathematical	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder`	`map` `instMin` `LinearMap.ker`	—	`strictMono_inf_prod_sup` `instIsModularLattice` `inf_comm` `map_lt_map_of_le_of_sup_lt_sup` `LT.lt.le`
`map_subtype_span_singleton` 📖	mathematical	—	`map` `Submodule` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `subtype` `span` `Set` `Set.instSingletonSet`	—	`RingHomSurjective.ids` `Set.image_congr` `Set.image_singleton`
`mapsTo_span` 📖	mathematical	`Set.MapsTo` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	`SetLike.coe` `Submodule` `setLike` `span`	—	`LE.le.trans` `span_mono` `span_preimage_le`
`mem_prod` 📖	mathematical	—	`Submodule` `Prod.instAddCommMonoid` `Prod.instModule` `SetLike.instMembership` `setLike` `prod`	—	`Set.mem_prod`
`notMem_span_of_apply_notMem_span_image` 📖	—	`Submodule` `SetLike.instMembership` `setLike` `span` `Set.image` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	—	—	`apply_mem_span_image_of_mem_span`
`prod_bot` 📖	mathematical	—	`prod` `Bot.bot` `Submodule` `instBot` `Prod.instAddCommMonoid` `Prod.instModule`	—	`ext`
`prod_coe` 📖	mathematical	—	`SetLike.coe` `Submodule` `Prod.instAddCommMonoid` `Prod.instModule` `setLike` `prod` `SProd.sprod` `Set` `Set.instSProd`	—	—
`prod_inf_prod` 📖	mathematical	—	`Submodule` `Prod.instAddCommMonoid` `Prod.instModule` `instMin` `prod`	—	`SetLike.coe_injective` `Set.prod_inter_prod`
`prod_mono` 📖	mathematical	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Prod.instAddCommMonoid` `Prod.instModule` `prod`	—	`Set.prod_mono`
`prod_sup_prod` 📖	mathematical	—	`Submodule` `Prod.instAddCommMonoid` `Prod.instModule` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `prod`	—	`le_antisymm` `sup_le` `prod_mono` `le_sup_left` `le_sup_right` `instIsConcreteLE` `mem_sup`
`prod_top` 📖	mathematical	—	`prod` `Top.top` `Submodule` `instTop` `Prod.instAddCommMonoid` `Prod.instModule`	—	`ext`
`singleton_span_isCompactElement` 📖	mathematical	—	`IsCompactElement` `Submodule` `instPartialOrder` `span` `Set` `Set.instSingletonSet`	—	`CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le` `SetLike.le_def` `instIsConcreteLE` `mem_span_singleton_self` `mem_sSup_of_directed`
`span_coe_eq_restrictScalars` 📖	mathematical	—	`span` `SetLike.coe` `Submodule` `setLike` `restrictScalars`	—	`span_eq`
`span_eq_top_of_span_eq_top` 📖	—	`span` `Top.top` `Submodule` `instTop`	—	—	`LE.le.antisymm` `le_top` `LE.le.trans` `Eq.ge` `span_le_restrictScalars`
`span_image` 📖	mathematical	—	`span` `Set.image` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike` `map`	—	`map_span`
`span_image_linearEquiv` 📖	mathematical	—	`span` `Set.image` `DFunLike.coe` `LinearEquiv` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `map` `RingHomSurjective.invPair` `LinearEquiv.toLinearMap`	—	`span_image` `RingHomSurjective.invPair`
`span_le_restrictScalars` 📖	mathematical	—	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `span` `restrictScalars`	—	`span_le` `subset_span`
`span_neg` 📖	mathematical	—	`span` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`RingHomSurjective.ids` `Set.image_congr` `Set.image_neg_eq_neg` `map_span` `map_neg` `map_id`
`span_preimage_le` 📖	mathematical	—	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `span` `Set.preimage` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike` `comap`	—	`span_le` `comap_coe` `Set.preimage_mono` `subset_span`
`span_prod_le` 📖	mathematical	—	`Submodule` `Prod.instAddCommMonoid` `Prod.instModule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `span` `SProd.sprod` `Set` `Set.instSProd` `prod`	—	`span_le` `Set.prod_mono` `subset_span`
`span_range_inclusionSpan` 📖	mathematical	—	`span` `Submodule` `SetLike.instMembership` `setLike` `SetLike.coe` `addCommMonoid` `module` `Set.range` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `module'` `LinearMap.instFunLike` `inclusionSpan` `Top.top` `instTop`	—	`Set.ext` `Set.image_congr` `subset_span` `map_injective_of_injective` `RingHomSurjective.ids` `injective_subtype` `map_subtype_top` `map_span`
`span_range_inclusion_eq_top` 📖	mathematical	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `restrictScalars` `span` `SetLike.coe` `setLike`	`SetLike.instMembership` `addCommMonoid` `restrictScalars.origModule` `Set.range` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `module` `LinearMap.instFunLike` `inclusion` `Top.top` `instTop`	—	`RingHomSurjective.ids` `map_span` `Set.ext` `Set.image_congr` `range_inclusion` `le_antisymm` `IsScalarTower.left` `span_coe_eq_restrictScalars` `restrictScalars_self` `span_mono` `map_injective_of_injective` `injective_subtype` `map_subtype_top`
`span_range_inclusion_restrictScalars_eq_top` 📖	mathematical	—	`span` `Submodule` `SetLike.instMembership` `setLike` `restrictScalars` `addCommMonoid` `restrictScalars.origModule` `Set.range` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `module` `LinearMap.instFunLike` `inclusion` `span_le_restrictScalars` `Top.top` `instTop`	—	`span_range_inclusion_eq_top` `span_le_restrictScalars` `span_span_of_tower`
`span_range_subtype_eq_top_iff` 📖	mathematical	`Submodule` `SetLike.instMembership` `setLike`	`span` `addCommMonoid` `module` `Set.range` `Top.top` `instTop`	—	`RingHomSurjective.ids` `map_injective_of_injective` `injective_subtype` `map_span` `Set.image_congr` `map_top` `range_subtype`
`span_singleton_eq_span_singleton` 📖	mathematical	—	`span` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instSingletonSet` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Units.instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Module.toDistribMulAction`	—	`eq_or_ne` `smul_zero` `smul_left_injective` `IsDomain.toIsCancelMulZero` `SemigroupAction.mul_smul` `one_smul` `smul_ne_zero_iff` `span_singleton_group_smul_eq` `Units.instIsScalarTower` `IsScalarTower.left`
`span_smul_eq_of_isUnit` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`span` `Set` `Set.smulSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Module.toDistribMulAction`	—	`le_antisymm` `span_smul_le` `smul_smul` `IsUnit.val_inv_mul` `one_smul`
`span_span_of_tower` 📖	mathematical	—	`span` `SetLike.coe` `Submodule` `setLike`	—	`le_antisymm` `span_le` `span_subset_span` `span_mono` `subset_span`
`span_subset_span` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `Submodule` `setLike` `span`	—	`span_le_restrictScalars`
`wcovBy_span_singleton_sup` 📖	mathematical	—	`WCovBy` `Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `PartialOrder.toPreorder` `instPartialOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `span` `Set` `Set.instSingletonSet`	—	`le_sup_right` `LT.lt.not_ge` `SetLike.exists_of_lt` `instIsConcreteLE` `LT.lt.le` `eq_or_ne` `zero_smul` `zero_add` `smul_mem_iff` `IsScalarTower.left` `add_mem_iff_left`

---

← Back to Index