Basic

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

Statistics

Metric	Count
Definitions	0
Theorems `comp_of_image`, `id_image`, `id_imageₛ`, `id_union`, `image`, `image_of_comp`, `map_injOn`, `union`, `LinearIndepOn_iff_linearIndepOn_image_injOn`, `disjoint_span_image`, `eq_coords_of_eq`, `eq_of_smul_apply_eq_smul_apply`, `fin_cons'`, `group_smul`, `group_smul_iff`, `linearCombination_ne_of_notMem_support`, `map`, `map'`, `map_injOn`, `map_of_injective_injective`, `map_of_injective_injectiveₛ`, `map_of_surjective_injective`, `map_of_surjective_injectiveₛ`, `notMem_span_image`, `restrict_scalars`, `restrict_scalars'`, `sum_type`, `units_smul`, `units_smul_iff`, `linearIndependent_iff`, `range_ker_disjoint`, `eq_of_linearIndepOn_id_of_span_subtype`, `le_of_span_le_span`, `linearIndepOn_congr`, `linearIndepOn_id_union_iff`, `linearIndepOn_of_finite`, `linearIndepOn_singleton_iff`, `linearIndepOn_union_iff`, `linearIndependent_finset_map_embedding_subtype`, `linearIndependent_monoidHom`, `linearIndependent_span`, `linearIndependent_subsingleton_index_iff`, `linearIndependent_sum`, `linearIndependent_unique`, `linearIndependent_unique_iff`, `span_le_span_iff`, `surjective_of_linearIndependent_of_span`	47
Total	47

LinearIndepOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_of_image` 📖	—	`LinearIndepOn` `Set.image` `Set.InjOn`	—	—	`LinearIndependent.comp` `Equiv.injective`
`id_image` 📖	mathematical	`LinearIndepOn`	`Set.image`	—	`image_of_comp`
`id_imageₛ` 📖	mathematical	`LinearIndepOn` `Set.InjOn` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `SetLike.coe` `Submodule` `Submodule.setLike` `Submodule.span`	`Set.image`	—	`id_image` `map_injOn` `Set.image_congr` `Set.image_id'`
`id_union` 📖	mathematical	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Disjoint` `Submodule` `Submodule.instPartialOrder` `Submodule.instOrderBot` `Submodule.span`	`Set` `Set.instUnion`	—	`union` `Set.image_congr` `Set.image_id'`
`image` 📖	mathematical	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Disjoint` `Submodule` `Submodule.instPartialOrder` `Submodule.instOrderBot` `Submodule.span` `LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring`	`Set.image` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	—	`id_imageₛ` `LinearMap.injOn_of_disjoint_ker` `le_rfl`
`image_of_comp` 📖	mathematical	`LinearIndepOn`	`Set.image`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Set.injOn_iff_injective` `Function.Injective.of_comp` `LinearIndependent.injective` `linearIndependent_equiv'`
`map_injOn` 📖	—	`LinearIndepOn` `Set.InjOn` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `SetLike.coe` `Submodule` `Submodule.setLike` `Submodule.span` `Set.image`	—	—	`LinearMap.linearIndepOn_iff_of_injOn`
`union` 📖	mathematical	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Disjoint` `Submodule` `Submodule.instPartialOrder` `Submodule.instOrderBot` `Submodule.span` `Set.image`	`Set` `Set.instUnion`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `LinearIndependent.sum_type` `Set.image_eq_range` `Disjoint.of_image` `Disjoint.of_span₀` `zero_notMem_image` `eq_1` `Equiv.Set.union_apply_left` `Equiv.Set.union_apply_right` `LinearIndependent.comp` `Equiv.injective`

LinearIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_span_image` 📖	mathematical	`LinearIndependent` `Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`Submodule` `Submodule.instPartialOrder` `Submodule.instOrderBot` `Submodule.span` `Set.image`	—	`Submodule.disjoint_def` `Finsupp.disjoint_supported_supported` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `finsuppLinearCombination_injective`
`eq_coords_of_eq` 📖	—	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Finset.sum` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—	`sub_eq_zero` `linearIndependent_iff'` `Finset.sum_congr` `Finset.sum_sub_distrib` `Finset.mem_univ`
`eq_of_smul_apply_eq_smul_apply` 📖	—	`LinearIndependent` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—	`Finsupp.sum_single_index` `zero_smul` `Finsupp.single_eq_single_iff`
`fin_cons'` 📖	mathematical	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Fin.cons`	—	`Fintype.linearIndependent_iff` `sum_mem` `Submodule.addSubmonoidClass` `Submodule.smul_mem` `Submodule.subset_span` `Finset.sum_congr` `Fin.cons_succ` `Fin.cons_zero` `Fin.sum_univ_succ` `zero_add` `zero_smul`
`group_smul` 📖	mathematical	`LinearIndependent`	`Pi.smul'`	—	`linearIndependent_iff''ₛ` `IsUnit.smul_left_cancel` `Group.isUnit` `Finset.sum_congr` `smul_assoc` `SMulCommClass.smul_comm`
`group_smul_iff` 📖	mathematical	—	`LinearIndependent` `Pi.smul'` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`inv_smul_smul` `group_smul`
`linearCombination_ne_of_notMem_support` 📖	—	`LinearIndependent` `Finset` `Finset.instMembership` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—	`RingHomSurjective.ids` `Finsupp.span_image_eq_map_linearCombination` `notMem_span_image` `Finsupp.mem_supported_support`
`map` 📖	mathematical	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Disjoint` `Submodule` `Submodule.instPartialOrder` `Submodule.instOrderBot` `Submodule.span` `Set.range` `LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring`	`DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	—	`LinearMap.linearIndependent_iff_of_disjoint`
`map'` 📖	mathematical	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring` `Bot.bot` `Submodule` `Submodule.instBot`	`DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	—	`map`
`map_injOn` 📖	—	`LinearIndependent` `Set.InjOn` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `SetLike.coe` `Submodule` `Submodule.setLike` `Submodule.span` `Set.range`	—	—	`LinearMap.linearIndependent_iff_of_injOn`
`map_of_injective_injective` 📖	—	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidHom.instFunLike` `SMulZeroClass.toSMul` `AddZero.toZero` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—	`linearIndependent_iff'` `AddMonoidHom.instAddMonoidHomClass` `Finset.sum_congr`
`map_of_injective_injectiveₛ` 📖	—	`LinearIndependent` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `SMulZeroClass.toSMul` `AddZero.toZero` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—	`linearIndependent_iff'ₛ` `AddMonoidHom.instAddMonoidHomClass` `Finset.sum_congr`
`map_of_surjective_injective` 📖	—	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `SMulZeroClass.toSMul` `AddZero.toZero` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—	`map_of_surjective_injectiveₛ` `injective_iff_map_eq_zero` `AddMonoidHom.instAddMonoidHomClass`
`map_of_surjective_injectiveₛ` 📖	—	`LinearIndependent` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.instFunLike` `SMulZeroClass.toSMul` `AddZero.toZero` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—	`Function.Surjective.hasRightInverse` `map_of_injective_injectiveₛ`
`notMem_span_image` 📖	mathematical	`LinearIndependent` `Set` `Set.instMembership`	`Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.image`	—	`Set.image_singleton` `Submodule.mem_span_singleton_self` `ne_zero` `Submodule.disjoint_def` `disjoint_span_image`
`restrict_scalars` 📖	—	`SMulZeroClass.toSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SMulWithZero.toSMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `LinearIndependent`	—	—	`zero_smul` `Finsupp.sum_mapRange_index` `smul_assoc` `one_smul` `Finsupp.ext`
`restrict_scalars'` 📖	—	`LinearIndependent`	—	—	`restrict_scalars` `faithfulSMul_iff_injective_smul_one`
`sum_type` 📖	—	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Disjoint` `Submodule` `Submodule.instPartialOrder` `Submodule.instOrderBot` `Submodule.span` `Set.range`	—	—	`linearIndependent_sum`
`units_smul` 📖	mathematical	`LinearIndependent`	`Pi.smul'` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Units.instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Module.toDistribMulAction`	—	`linearIndependent_iff''ₛ` `Finset.sum_congr` `SemigroupAction.mul_smul`
`units_smul_iff` 📖	mathematical	—	`LinearIndependent` `Pi.smul'` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Units.instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Module.toDistribMulAction`	—	`inv_smul_smul` `units_smul`

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`linearIndependent_iff` 📖	mathematical	`ker` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `Bot.bot` `Submodule` `Submodule.instBot`	`LinearIndependent` `DFunLike.coe` `LinearMap` `instFunLike`	—	`linearIndependent_iff_of_disjoint`

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`range_ker_disjoint` 📖	mathematical	`LinearIndependent` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`Disjoint` `Submodule` `instPartialOrder` `instOrderBot` `span` `Set.range` `LinearMap.ker`	—	`disjoint_iff_inf_le` `Set.image_univ` `RingHomSurjective.ids` `Finsupp.span_image_eq_map_linearCombination` `map_inf_eq_map_inf_comap` `RingHomCompTriple.ids` `LinearMap.ker_comp` `LinearMap.ker_eq_bot_of_injective` `Finsupp.linearCombination_linear_comp` `LinearIndependent.eq_1` `inf_bot_eq` `map_bot` `le_refl`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`LinearIndepOn_iff_linearIndepOn_image_injOn` 📖	mathematical	—	`LinearIndepOn` `Set.image` `Set.InjOn`	—	`LinearIndepOn.id_image` `LinearIndepOn.injOn` `linearIndepOn_iff_image`
`eq_of_linearIndepOn_id_of_span_subtype` 📖	—	`LinearIndepOn` `Set` `Set.instHasSubset` `SetLike.coe` `Submodule` `Submodule.setLike` `Submodule.span`	—	—	`Subtype.coe_injective` `surjective_of_linearIndependent_of_span` `Subtype.range_coe_subtype` `Set.Subset.antisymm` `Subtype.mem`
`le_of_span_le_span` 📖	—	`LinearIndepOn` `Set` `Set.instHasSubset` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.span`	—	—	`eq_of_linearIndepOn_id_of_span_subtype` `LinearIndepOn.mono` `Set.union_subset` `Set.subset_union_right` `Set.Subset.trans` `Submodule.subset_span` `Set.subset_union_left`
`linearIndepOn_congr` 📖	mathematical	`Set.EqOn`	`LinearIndepOn`	—	`LinearIndepOn.eq_1` `Set.EqOn.symm`
`linearIndepOn_id_union_iff` 📖	mathematical	`Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set.instUnion` `Submodule` `Submodule.instPartialOrder` `Submodule.instOrderBot` `Submodule.span`	—	`linearIndepOn_union_iff` `Set.image_id`
`linearIndepOn_of_finite` 📖	—	`LinearIndepOn`	—	—	`linearIndepOn_iffₛ` `Set.union_subset` `Set.Finite.union` `Finset.finite_toSet` `Set.subset_union_left` `Set.subset_union_right`
`linearIndepOn_singleton_iff` 📖	mathematical	—	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instSingletonSet`	—	`LinearIndepOn.ne_zero` `IsDomain.toNontrivial` `LinearIndepOn.singleton`
`linearIndepOn_union_iff` 📖	mathematical	`Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set.instUnion` `Submodule` `Submodule.instPartialOrder` `Submodule.instOrderBot` `Submodule.span` `Set.image`	—	`LinearIndepOn.mono` `Set.subset_union_left` `Set.subset_union_right` `Set.ext` `LinearIndependent.disjoint_span_image` `Disjoint.preimage` `LinearIndepOn.union`
`linearIndependent_finset_map_embedding_subtype` 📖	mathematical	`LinearIndependent` `Set` `Set.instMembership`	`Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.map` `Function.Embedding.subtype`	—	`LinearIndependent.comp`
`linearIndependent_monoidHom` 📖	mathematical	—	`LinearIndependent` `MonoidHom` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `MonoidHom.instFunLike` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Pi.Function.module` `Semiring.toModule`	—	`linearIndependent_iff'` `Finset.induction_on` `instIsEmptyFalse` `sub_eq_zero` `Finset.sum_apply` `Finset.sum_congr` `sub_mul` `Finset.sum_sub_distrib` `Finset.sum_insert` `add_sub_add_left_eq_sub` `mul_assoc` `mul_left_comm` `map_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass` `Finset.mul_sum` `MulZeroClass.mul_zero` `sub_self` `MonoidHom.ext` `smul_eq_zero` `instIsTorsionFree` `IsDomain.toIsCancelMulZero` `smul_sub` `sub_ne_zero_of_ne` `mul_one` `MonoidHom.map_one` `Finset.sum_eq_zero` `zero_smul` `add_zero` `Finset.forall_mem_insert`
`linearIndependent_span` 📖	mathematical	`LinearIndependent`	`Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `Submodule.subset_span` `Set.mem_range_self` `Submodule.addCommMonoid` `Submodule.module`	—	`LinearIndependent.of_comp` `Submodule.subset_span` `Set.mem_range_self`
`linearIndependent_subsingleton_index_iff` 📖	mathematical	—	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`isEmpty_or_nonempty` `unique_iff_subsingleton_and_nonempty` `linearIndependent_unique_iff` `Unique.eq_default`
`linearIndependent_sum` 📖	mathematical	—	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Disjoint` `Submodule` `Submodule.instPartialOrder` `Submodule.instOrderBot` `Submodule.span` `Set.range`	—	`Set.range_comp` `LinearIndependent.comp` `Sum.inl_injective` `Sum.inr_injective` `LinearIndependent.disjoint_span_image` `IsCompl.disjoint` `Set.isCompl_range_inl_range_inr` `linearIndependent_iff'` `Function.Injective.injOn` `Finset.sum_preimage'` `Finset.sum_union` `Finset.disjoint_filter` `Set.disjoint_left` `Finset.filter_or` `Finset.sum_congr` `Finset.filter.congr_simp` `Set.range_inl_union_range_inr` `Finset.filter_true` `Submodule.disjoint_def'` `sum_mem` `Submodule.addSubmonoidClass` `Submodule.smul_mem` `Submodule.subset_span` `Set.mem_range_self` `NegMemClass.neg_mem` `AddSubgroupClass.toNegMemClass` `Submodule.addSubgroupClass` `eq_neg_iff_add_eq_zero` `Finset.mem_preimage` `neg_eq_zero`
`linearIndependent_unique` 📖	mathematical	—	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`linearIndependent_unique_iff`
`linearIndependent_unique_iff` 📖	mathematical	—	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`Finsupp.linearCombination_unique` `IsDomain.toIsCancelMulZero` `Finsupp.single_eq_same` `NeZero.one` `IsDomain.toNontrivial` `LinearIndependent.of_subsingleton` `Unique.instSubsingleton`
`span_le_span_iff` 📖	mathematical	`LinearIndependent` `Set` `Set.instMembership` `Set.instHasSubset`	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.span`	—	`le_of_span_le_span` `Submodule.span_mono`
`surjective_of_linearIndependent_of_span` 📖	—	`LinearIndependent` `Set` `Set.instHasSubset` `Set.range` `SetLike.coe` `Submodule` `Submodule.setLike` `Submodule.span` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	—	—	`LinearIndependent.comp` `Function.Embedding.injective` `Set.mem_range_self` `Finsupp.linearCombination_mapDomain` `LinearIndependent.linearCombination_repr` `Finsupp.linearCombination_single` `one_smul` `Finsupp.single_of_embDomain_single` `zero_ne_one` `NeZero.one` `Finsupp.embDomain_eq_mapDomain`

---

← Back to Index