Defs

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

Statistics

Metric	Count
Definitions `LinearIndepOn`, `linearCombinationEquiv`, `repr`	3
Theorems `linearIndependent_iff`, `linearIndependent_iffₒₛ`, `linearIndependent_iffₛ`, `not_linearIndependent_iff`, `not_linearIndependent_iffₒₛ`, `not_linearIndependent_iffₛ`, `eq_zero_of_smul_mem_span`, `id_singleton`, `injOn`, `linearIndependent`, `linearIndependent_restrict`, `mono`, `ne_zero`, `notMem_span`, `notMem_span_of_insert`, `of_comp`, `of_subsingleton`, `singleton`, `singleton'`, `zero_notMem_image`, `comp`, `eq_zero_of_smul_mem_span`, `finsuppLinearCombination_injective`, `fintypeLinearCombination_injective`, `injective`, `linearCombinationEquiv_apply_coe`, `linearCombinationEquiv_symm_apply`, `linearCombination_comp_repr`, `linearCombination_repr`, `linearIndepOn`, `linearIndepOn_id`, `linearIndepOn_id'`, `maximal_iff`, `ne_zero`, `notMem_span`, `of_comp`, `of_linearIndepOn_id_range`, `of_linearIndepOn_range`, `of_subsingleton`, `of_subsingleton'`, `repr_eq`, `repr_eq_single`, `repr_ker`, `repr_range`, `smul_left_injective`, `span_repr_eq`, `linearIndepOn_iff_of_injOn`, `linearIndependent_iff_of_disjoint`, `linearIndependent_iff_of_injOn`, `linearDepOn_iff`, `linearDepOn_iff'`, `linearDepOn_iff'ₛ`, `linearDepOn_iffₛ`, `linearIndepOn_empty`, `linearIndepOn_equiv`, `linearIndepOn_finset_iff`, `linearIndepOn_finset_iffₒₛ`, `linearIndepOn_finset_iffₛ`, `linearIndepOn_id_range_iff`, `linearIndepOn_iff`, `linearIndepOn_iff'`, `linearIndepOn_iff''`, `linearIndepOn_iff_disjoint`, `linearIndepOn_iff_image`, `linearIndepOn_iff_linearCombinationOn`, `linearIndepOn_iff_linearCombinationOnₛ`, `linearIndepOn_iff_linearIndepOn_finset`, `linearIndepOn_iff_notMem_span`, `linearIndepOn_iffₛ`, `linearIndepOn_range_iff`, `linearIndepOn_univ`, `linearIndepOn_zero_iff`, `linearIndependent_add_smul_iff`, `linearIndependent_comp_subtype_iff`, `linearIndependent_empty`, `linearIndependent_empty_type`, `linearIndependent_equiv`, `linearIndependent_equiv'`, `linearIndependent_iff`, `linearIndependent_iff'`, `linearIndependent_iff''`, `linearIndependent_iff''ₛ`, `linearIndependent_iff'ₛ`, `linearIndependent_iff_eq_zero_of_smul_mem_span`, `linearIndependent_iff_finset_linearIndependent`, `linearIndependent_iff_injective_finsuppLinearCombination`, `linearIndependent_iff_injective_fintypeLinearCombination`, `linearIndependent_iff_ker`, `linearIndependent_iff_notMem_span`, `linearIndependent_iffₒₛ`, `linearIndependent_iffₛ`, `linearIndependent_of_subsingleton`, `linearIndependent_restrict_iff`, `linearIndependent_set_coe_iff`, `linearIndependent_subsingleton_iff`, `linearIndependent_subtype_iff`, `linearIndependent_zero_iff`, `not_linearIndepOn_finset_iff`, `not_linearIndepOn_finset_iffₒₛ`, `not_linearIndepOn_finset_iffₛ`, `not_linearIndependent_iff`, `not_linearIndependent_iffₒₛ`, `not_linearIndependent_iffₛ`	103
Total	106

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`linearIndependent_iff` 📖	mathematical	—	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`linearIndependent_iff'` `linearIndependent_iff''` `Finset.sum_subset` `Finset.subset_univ` `zero_smul`
`linearIndependent_iffₒₛ` 📖	mathematical	—	`LinearIndependent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`linearIndependent_iffₒₛ` `disjoint_compl_right` `Finset.mem_compl` `Finset.sum_subset` `Disjoint.le_compl_left` `zero_smul` `Finset.sum_congr`
`linearIndependent_iffₛ` 📖	mathematical	—	`LinearIndependent`	—	—
`not_linearIndependent_iff` 📖	mathematical	—	`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` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`not_iff_not` `linearIndependent_iff`
`not_linearIndependent_iffₒₛ` 📖	mathematical	—	`LinearIndependent` `Finset.sum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Compl.compl` `Finset` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `Finset.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Finset.sum_congr` `compl_compl` `Finset.mem_compl`
`not_linearIndependent_iffₛ` 📖	mathematical	—	`LinearIndependent` `Finset.sum` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`not_iff_not` `linearIndependent_iffₛ`

LinearIndepOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_zero_of_smul_mem_span` 📖	mathematical	`LinearIndepOn` `Set` `Set.instMembership` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.image` `Set.instSDiff` `Set.instSingletonSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`LinearIndependent.eq_zero_of_smul_mem_span` `Set.image_comp` `Set.image_diff` `Subtype.val_injective` `Set.image_univ` `Subtype.range_coe_subtype` `Set.image_singleton`
`id_singleton` 📖	mathematical	—	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instSingletonSet`	—	`singleton`
`injOn` 📖	mathematical	`LinearIndepOn`	`Set.InjOn`	—	`Set.injOn_iff_injective` `LinearIndependent.injective`
`linearIndependent` 📖	mathematical	`LinearIndepOn`	`LinearIndependent` `Set.Elem` `Set` `Set.instMembership`	—	—
`linearIndependent_restrict` 📖	mathematical	`LinearIndepOn`	`LinearIndependent` `Set.Elem` `Set.restrict`	—	—
`mono` 📖	—	`LinearIndepOn` `Set` `Set.instHasSubset`	—	—	`LinearIndependent.comp` `Set.inclusion_injective`
`ne_zero` 📖	—	`LinearIndepOn` `Set` `Set.instMembership`	—	—	`LinearIndependent.ne_zero`
`notMem_span` 📖	mathematical	`LinearIndepOn` `Set` `Set.instMembership`	`Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.image` `Set.instSDiff` `Set.instSingletonSet`	—	`one_ne_zero` `NeZero.one` `eq_zero_of_smul_mem_span` `one_smul`
`notMem_span_of_insert` 📖	mathematical	`LinearIndepOn` `Set` `Set.instInsert` `Set.instMembership`	`Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.image`	—	`Set.insert_diff_of_mem` `Set.diff_singleton_eq_self` `notMem_span` `Set.mem_insert`
`of_comp` 📖	—	`LinearIndepOn` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	—	—	`LinearIndependent.of_comp`
`of_subsingleton` 📖	mathematical	—	`LinearIndepOn`	—	`linearIndependent_of_subsingleton`
`singleton` 📖	mathematical	—	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instSingletonSet`	—	`IsDomain.toIsCancelMulZero`
`singleton'` 📖	mathematical	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instSingletonSet`	—	`LinearIndependent.of_subsingleton'` `Unique.instSubsingleton`
`zero_notMem_image` 📖	mathematical	`LinearIndepOn`	`Set` `Set.instMembership` `Set.image` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`ne_zero`

LinearIndependent

Definitions

Name	Category	Theorems
`linearCombinationEquiv` 📖	CompOp	2 math math: `linearCombinationEquiv_apply_coe`, `linearCombinationEquiv_symm_apply`
`repr` 📖	CompOp	13 math math: `linearCombination_repr`, `Module.Basis.mk_repr`, `setBasisOfLinearIndependentOfCardEqFinrank_repr_apply`, `repr_eq_single`, `basisOfLinearIndependentOfCardEqFinrank_repr_apply`, `linearCombination_comp_repr`, `finsetBasisOfTopLeSpanOfCardEqFinrank_repr_apply`, `span_repr_eq`, `repr_range`, `setBasisOfTopLeSpanOfCardEqFinrank_repr_apply`, `repr_eq`, `repr_ker`, `finsetBasisOfLinearIndependentOfCardEqFinrank_repr_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`LinearIndependent`	—	—	`Finsupp.linearCombination_mapDomain` `Finsupp.mapDomain_injective`
`eq_zero_of_smul_mem_span` 📖	mathematical	`LinearIndependent` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.image` `Set` `Set.instSDiff` `Set.univ` `Set.instSingletonSet` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`RingHomSurjective.ids` `Submodule.mem_map` `Finsupp.span_image_eq_map_linearCombination` `Set.notMem_of_mem_diff` `linearIndependent_iffₛ` `Finsupp.linearCombination_single` `Finsupp.single_eq_same` `Set.mem_singleton`
`finsuppLinearCombination_injective` 📖	mathematical	`LinearIndependent`	`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`	—	`linearIndependent_iff_injective_finsuppLinearCombination`
`fintypeLinearCombination_injective` 📖	mathematical	`LinearIndependent`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `Fintype.linearCombination`	—	`linearIndependent_iff_injective_fintypeLinearCombination`
`injective` 📖	—	`LinearIndependent`	—	—	`Finsupp.linearCombination_single` `one_smul` `Finsupp.single_left_injective` `one_ne_zero` `NeZero.one`
`linearCombinationEquiv_apply_coe` 📖	mathematical	`LinearIndependent`	`Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Submodule.addCommMonoid` `Finsupp.module` `Semiring.toModule` `Submodule.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `linearCombinationEquiv` `LinearMap` `LinearMap.instFunLike` `Finsupp.linearCombination`	—	`RingHomInvPair.ids`
`linearCombinationEquiv_symm_apply` 📖	mathematical	`LinearIndependent`	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Submodule.addCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Submodule.module` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `linearCombinationEquiv` `Equiv.invFun` `Equiv.trans` `LinearMap.range` `RingHomSurjective.invPair` `LinearMap.codRestrict` `Finsupp.linearCombination` `LinearEquiv.toEquiv` `LinearEquiv.ofInjective` `LinearEquiv.ofTop`	—	`RingHomInvPair.ids`
`linearCombination_comp_repr` 📖	mathematical	`LinearIndependent`	`LinearMap.comp` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Submodule.addCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Submodule.module` `Finsupp.module` `Semiring.toModule` `RingHom.id` `RingHomCompTriple.ids` `Finsupp.linearCombination` `repr` `Submodule.subtype`	—	`LinearMap.ext` `RingHomCompTriple.ids` `linearCombination_repr`
`linearCombination_repr` 📖	mathematical	`LinearIndependent`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `LinearMap.instFunLike` `Finsupp.linearCombination` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `Submodule.addCommMonoid` `Submodule.module` `repr`	—	`RingHomInvPair.ids` `LinearEquiv.apply_symm_apply`
`linearIndepOn` 📖	mathematical	`LinearIndependent`	`LinearIndepOn` `Set.univ`	—	`linearIndepOn_univ`
`linearIndepOn_id` 📖	mathematical	`LinearIndependent`	`LinearIndepOn` `Set.range`	—	`Set.comp_rangeSplitting` `comp` `Set.rangeSplitting_injective`
`linearIndepOn_id'` 📖	mathematical	`LinearIndependent` `Set.range`	`LinearIndepOn`	—	`linearIndepOn_id`
`maximal_iff` 📖	mathematical	`LinearIndependent`	`Maximal`	—	`Set.range_eq_univ` `Set.image_injective` `injective` `Set.image_univ` `Set.range_comp` `linearIndepOn_id` `Set.range_comp_subset_range` `Set.range_subset_iff` `Function.Surjective.range_eq` `Set.image_congr` `Subtype.range_coe_subtype` `Set.image_image`
`ne_zero` 📖	—	`LinearIndependent`	—	—	`Finsupp.linearCombination_single` `one_smul` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `NeZero.one`
`notMem_span` 📖	mathematical	`LinearIndependent`	`Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.image` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	—	`one_ne_zero` `NeZero.one` `eq_zero_of_smul_mem_span` `one_smul` `Set.compl_eq_univ_diff`
`of_comp` 📖	—	`LinearIndependent` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	—	—	`Function.Injective.of_comp` `RingHomCompTriple.ids` `LinearMap.coe_comp` `Finsupp.linearCombination_linear_comp` `eq_1`
`of_linearIndepOn_id_range` 📖	mathematical	`LinearIndepOn` `Set.range`	`LinearIndependent`	—	`linearIndepOn_id_range_iff`
`of_linearIndepOn_range` 📖	mathematical	`LinearIndepOn` `Set.range`	`LinearIndependent`	—	`linearIndepOn_range_iff`
`of_subsingleton` 📖	mathematical	—	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`of_subsingleton'` `IsDomain.toIsCancelMulZero`
`of_subsingleton'` 📖	mathematical	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`Finsupp.linearCombination_unique`
`repr_eq` 📖	mathematical	`LinearIndependent` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `LinearMap.instFunLike` `Finsupp.linearCombination` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range`	`Submodule.addCommMonoid` `Submodule.module` `repr`	—	`RingHomInvPair.ids` `LinearEquiv.symm_apply_apply`
`repr_eq_single` 📖	mathematical	`LinearIndependent` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Submodule.addCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Submodule.module` `Finsupp.module` `Semiring.toModule` `LinearMap.instFunLike` `repr` `Finsupp.single` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`repr_eq` `Finsupp.linearCombination_single` `one_smul`
`repr_ker` 📖	mathematical	`LinearIndependent`	`LinearMap.ker` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Submodule.addCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Submodule.module` `Finsupp.module` `Semiring.toModule` `RingHom.id` `repr` `Bot.bot` `Submodule.instBot`	—	`RingHomInvPair.ids` `repr.eq_1` `LinearEquiv.ker`
`repr_range` 📖	mathematical	`LinearIndependent`	`LinearMap.range` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Submodule.addCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Submodule.module` `Finsupp.module` `Semiring.toModule` `RingHom.id` `RingHomSurjective.ids` `repr` `Top.top` `Submodule.instTop`	—	`RingHomSurjective.ids` `RingHomInvPair.ids` `repr.eq_1` `RingHomSurjective.invPair` `LinearEquiv.range`
`smul_left_injective` 📖	mathematical	`LinearIndependent`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`Finsupp.linearCombination_single` `Finsupp.single_injective`
`span_repr_eq` 📖	mathematical	`LinearIndependent`	`Span.repr` `Set.range` `Finsupp.equivMapDomain` `Set.Elem` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Equiv.ofInjective` `injective` `DFunLike.coe` `LinearMap` `RingHom.id` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Finsupp` `Submodule.addCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Submodule.module` `Finsupp.module` `Semiring.toModule` `LinearMap.instFunLike` `repr`	—	`injective` `LinearEquiv.injective` `RingHomInvPair.ids` `Finsupp.linearCombination_equivMapDomain` `Equiv.self_comp_ofInjective_symm` `Span.finsupp_linearCombination_repr` `linearCombination_repr` `Finsupp.ext` `Equiv.ofInjective_symm_apply`

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`linearIndepOn_iff_of_injOn` 📖	mathematical	`Set.InjOn` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike` `SetLike.coe` `Submodule` `Submodule.setLike` `Submodule.span` `Set.image`	`LinearIndepOn`	—	`linearIndependent_iff_of_injOn` `Set.image_eq_range`
`linearIndependent_iff_of_disjoint` 📖	mathematical	`Disjoint` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `Submodule.instOrderBot` `Submodule.span` `Set.range` `ker` `RingHom.id` `Semiring.toNonAssocSemiring`	`LinearIndependent` `DFunLike.coe` `LinearMap` `instFunLike`	—	`linearIndependent_iff_of_injOn` `injOn_of_disjoint_ker` `le_rfl`
`linearIndependent_iff_of_injOn` 📖	mathematical	`Set.InjOn` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike` `SetLike.coe` `Submodule` `Submodule.setLike` `Submodule.span` `Set.range`	`LinearIndependent`	—	`RingHomCompTriple.ids` `Finsupp.linearCombination_linear_comp` `Set.InjOn.injective_iff` `RingHomSurjective.ids` `Finsupp.range_linearCombination` `coe_range` `subset_refl` `Set.instReflSubset`

(root)

Definitions

Name	Category	Theorems
`LinearIndepOn` 📖	MathDef	71 math math: `linearIndependent_set_coe_iff`, `Module.rank_def`, `RootPairing.linearIndepOn_root_baseOf'`, `linearIndepOn_iff_notMem_span`, `exists_set_linearIndependent_of_isDomain`, `linearIndepOn_finset_iff`, `LinearMap.le_rank_iff_exists_linearIndependent`, `LinearMap.linearIndepOn_iff_of_injOn`, `RootPairing.Base.linearIndepOn_coroot`, `linearIndepOn_id_union_iff`, `linearIndepOn_univ`, `linearIndepOn_finset_iffₒₛ`, `linearIndepOn_iff`, `LinearIndepOn.of_subsingleton`, `linearIndependent_comp_subtype_iff`, `linearIndepOn_iffₛ`, `linearIndependent_restrict_iff`, `linearIndepOn_id_insert_iff`, `linearIndepOn_singleton_iff`, `linearIndepOn_iff''`, `Module.le_rank_iff_exists_finset`, `linearIndepOn_id_range_iff`, `linearIndepOn_pair_iff`, `LinearIndependent.linearIndepOn_id`, `exists_maximal_linearIndepOn'`, `linearDepOn_iff`, `LinearIndependent.linearIndepOn`, `linearIndepOn_iff_disjoint`, `isProperLinearSet_iff`, `linearIndependent_subtype_iff`, `linearIndepOn_range_iff`, `RootPairing.linearIndepOn_root_baseOf`, `le_rank_iff_exists_linearIndependent`, `RootPairing.Base.linearIndepOn_root`, `LinearIndepOn.id_singleton`, `linearIndepOn_id_pair`, `exists_finset_linearIndependent_of_le_rank`, `linearIndepOn_union_iff`, `linearIndepOn_congr`, `LinearIndepOn.singleton'`, `linearIndepOn_empty`, `linearIndepOn_finset_iffₛ`, `Submodule.exists_finset_span_eq_linearIndepOn`, `RootPairing.linearIndepOn_coroot_iff`, `linearIndepOn_zero_iff`, `RootPairing.eq_baseOf_iff`, `linearIndepOn_equiv`, `nonempty_linearIndependent_set`, `exists_maximal_linearIndepOn`, `linearIndepOn_iff'`, `linearIndepOn_iff_linearIndepOn_finset`, `LinearIndependent.linearIndepOn_id'`, `not_linearIndepOn_finset_iff`, `linearIndepOn_iff_image`, `exists_set_linearIndependent_of_lt_rank`, `linearDepOn_iffₛ`, `linearIndepOn_union_iff_quotient`, `not_linearIndepOn_finset_iffₛ`, `linearIndepOn_insert`, `LinearIndepOn_iff_linearIndepOn_image_injOn`, `linearIndepOn_id_insert`, `LinearIndepOn.singleton`, `HasRankNullity.exists_set_linearIndependent`, `not_linearIndepOn_finset_iffₒₛ`, `linearDepOn_iff'`, `linearIndepOn_isGroupLikeElem`, `linearIndepOn_insert_iff`, `LinearIndepOn.pair_iff`, `linearDepOn_iff'ₛ`, `linearIndepOn_iff_linearCombinationOnₛ`, `linearIndepOn_iff_linearCombinationOn`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`linearDepOn_iff` 📖	mathematical	—	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Submodule` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.instAddCommMonoid` `Finsupp.module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `Finsupp.supported` `Finset.sum` `Finsupp.support` `SMulZeroClass.toSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `DFunLike.coe` `Finsupp.instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`linearDepOn_iff'`
`linearDepOn_iff'` 📖	mathematical	—	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Submodule` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.instAddCommMonoid` `Finsupp.module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `Finsupp.supported` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.instFunLike` `Finsupp.linearCombination` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—
`linearDepOn_iff'ₛ` 📖	mathematical	—	`LinearIndepOn` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Submodule` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.instAddCommMonoid` `Finsupp.module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `Finsupp.supported` `DFunLike.coe` `LinearMap` `RingHom.id` `LinearMap.instFunLike` `Finsupp.linearCombination`	—	—
`linearDepOn_iffₛ` 📖	mathematical	—	`LinearIndepOn` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Submodule` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.instAddCommMonoid` `Finsupp.module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `Finsupp.supported` `Finset.sum` `Finsupp.support` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `DFunLike.coe` `Finsupp.instFunLike`	—	`linearDepOn_iff'ₛ`
`linearIndepOn_empty` 📖	mathematical	—	`LinearIndepOn` `Set` `Set.instEmptyCollection`	—	`linearIndependent_empty_type` `Set.instIsEmptyElemEmptyCollection`
`linearIndepOn_equiv` 📖	mathematical	—	`LinearIndepOn` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Set.image`	—	`linearIndependent_equiv'`
`linearIndepOn_finset_iff` 📖	mathematical	—	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.coe` `Finset` `Finset.instSetLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`Finset.sum_attach` `Subtype.coe_eta` `dite_smul` `zero_smul` `Finset.sum_congr`
`linearIndepOn_finset_iffₒₛ` 📖	mathematical	—	`LinearIndepOn` `SetLike.coe` `Finset` `Finset.instSetLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`LinearIndepOn.eq_1` `Fintype.linearIndependent_iffₒₛ` `Finset.sum_congr` `Finset.sum_filter` `Finset.compl_filter` `Finset.sum_coe_sort` `Finset.sum_ite_mem` `Finset.inter_eq_right` `Finset.sum_ite` `Finset.sum_const_zero` `Finset.filter_notMem_eq_sdiff` `zero_add` `Subtype.coe_eta` `Finset.map_subtype_subset` `Finset.subtype_map_of_mem` `Finset.subtype_eq_univ` `Finset.map_sdiff` `dite_smul` `zero_smul` `Finset.sum_map`
`linearIndepOn_finset_iffₛ` 📖	mathematical	—	`LinearIndepOn` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`Finset.sum_attach` `Subtype.coe_eta` `dite_smul` `zero_smul` `Finset.sum_congr`
`linearIndepOn_id_range_iff` 📖	mathematical	—	`LinearIndepOn` `Set.range` `LinearIndependent`	—	`linearIndepOn_range_iff`
`linearIndepOn_iff` 📖	mathematical	—	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finsupp.instZero`	—	`linearIndepOn_iffₛ` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `sub_eq_zero` `sub_mem` `Submodule.addSubgroupClass` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `sub_self`
`linearIndepOn_iff'` 📖	mathematical	—	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`LinearIndepOn.eq_1` `linearIndependent_iff'` `Function.Injective.injOn` `Subtype.val_injective` `Finset.sum_preimage` `Subtype.range_coe_subtype` `Finset.coe_image` `Subtype.coe_preimage_self` `Finset.sum_congr` `dite_smul` `zero_smul` `Finset.sum_image` `Subtype.coe_eta`
`linearIndepOn_iff''` 📖	mathematical	—	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`linearIndepOn_iff'` `Finset.sum_congr`
`linearIndepOn_iff_disjoint` 📖	mathematical	—	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Disjoint` `Submodule` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finsupp.instAddCommMonoid` `Finsupp.module` `Semiring.toModule` `Submodule.instPartialOrder` `Submodule.instOrderBot` `Finsupp.supported` `LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp.linearCombination`	—	`linearIndepOn_iff` `LinearMap.disjoint_ker`
`linearIndepOn_iff_image` 📖	mathematical	`Set.InjOn`	`LinearIndepOn` `Set.image`	—	`linearIndependent_equiv'`
`linearIndepOn_iff_linearCombinationOn` 📖	mathematical	—	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.ker` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Submodule` `Finsupp.instAddCommMonoid` `Finsupp.module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `Finsupp.supported` `Submodule.span` `Set.image` `Submodule.addCommMonoid` `Submodule.module` `RingHom.id` `Finsupp.linearCombinationOn` `Bot.bot` `Submodule.instBot`	—	`linearIndepOn_iff_linearCombinationOnₛ` `LinearMap.ker_eq_bot`
`linearIndepOn_iff_linearCombinationOnₛ` 📖	mathematical	—	`LinearIndepOn` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Submodule` `Finsupp.instAddCommMonoid` `Finsupp.module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `Finsupp.supported` `Submodule.span` `Set.image` `DFunLike.coe` `LinearMap` `RingHom.id` `Submodule.addCommMonoid` `Submodule.module` `LinearMap.instFunLike` `Finsupp.linearCombinationOn`	—	`linearIndependent_restrict_iff` `RingHomInvPair.ids` `RingHomCompTriple.ids` `Finsupp.linearCombination_restrict`
`linearIndepOn_iff_linearIndepOn_finset` 📖	mathematical	—	`LinearIndepOn` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`LinearIndepOn.mono` `LinearIndepOn.eq_1` `linearIndependent_iff_finset_linearIndependent` `LinearIndependent.comp` `Finset.coe_map` `Set.image_congr` `Subtype.coe_preimage_self` `Finset.mem_map_of_mem`
`linearIndepOn_iff_notMem_span` 📖	mathematical	—	`LinearIndepOn` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.image` `Set` `Set.instSDiff` `Set.instSingletonSet`	—	`LinearIndepOn.eq_1` `linearIndependent_iff_notMem_span` `Set.image_comp` `Set.image_diff` `Subtype.val_injective` `Set.image_univ` `Subtype.range_coe_subtype` `Set.image_singleton`
`linearIndepOn_iffₛ` 📖	mathematical	—	`LinearIndepOn`	—	`Finsupp.subtypeDomain_eq_iff` `Finsupp.sum_subtypeDomain_index` `Finsupp.embDomain_injective` `Finsupp.embDomain_eq_mapDomain` `Finsupp.sum_mapDomain_index` `zero_smul` `add_smul`
`linearIndepOn_range_iff` 📖	mathematical	—	`LinearIndepOn` `Set.range` `LinearIndependent`	—	`linearIndependent_equiv'`
`linearIndepOn_univ` 📖	mathematical	—	`LinearIndepOn` `Set.univ` `LinearIndependent`	—	`linearIndependent_equiv'`
`linearIndepOn_zero_iff` 📖	mathematical	—	`LinearIndepOn` `Pi.instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Set` `Set.instEmptyCollection`	—	`linearIndependent_zero_iff` `Set.isEmpty_coe_sort`
`linearIndependent_add_smul_iff` 📖	mathematical	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`LinearIndependent` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `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`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `Finsupp.linearCombination_comp_addSingleEquiv`
`linearIndependent_comp_subtype_iff` 📖	mathematical	—	`LinearIndependent` `Set.Elem` `Set` `Set.instMembership` `LinearIndepOn`	—	—
`linearIndependent_empty` 📖	mathematical	—	`LinearIndependent` `Set.Elem` `Set` `Set.instEmptyCollection` `Set.instMembership`	—	`linearIndependent_empty_type` `Set.instIsEmptyElemEmptyCollection`
`linearIndependent_empty_type` 📖	mathematical	—	`LinearIndependent`	—	`Function.injective_of_subsingleton` `Unique.instSubsingleton`
`linearIndependent_equiv` 📖	mathematical	—	`LinearIndependent` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`LinearIndependent.comp` `Equiv.injective` `Equiv.self_comp_symm`
`linearIndependent_equiv'` 📖	mathematical	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	`LinearIndependent`	—	`linearIndependent_equiv`
`linearIndependent_iff` 📖	mathematical	—	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instZero`	—	—
`linearIndependent_iff'` 📖	mathematical	—	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`linearIndependent_iff'ₛ` `Finset.sum_congr` `zero_smul` `Finset.sum_const_zero` `sub_eq_zero` `Finset.sum_sub_distrib` `sub_smul`
`linearIndependent_iff''` 📖	mathematical	—	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`linearIndependent_iff'` `Finset.sum_congr` `ite_smul` `zero_smul` `Finset.sum_extend_by_zero`
`linearIndependent_iff''ₛ` 📖	mathematical	—	`LinearIndependent`	—	`linearIndependent_iff'ₛ` `Finset.sum_congr` `ite_smul` `zero_smul` `Finset.sum_extend_by_zero`
`linearIndependent_iff'ₛ` 📖	mathematical	—	`LinearIndependent`	—	`linearIndependent_iffₛ` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Finset.sum_congr` `Finsupp.linearCombination_single` `Finsupp.lapply_apply` `Finsupp.single_eq_same` `Finset.sum_eq_single` `Finsupp.single_eq_of_ne'` `Finsupp.ext` `by_contradiction` `Finset.sum_subset` `Finset.subset_union_left` `Finsupp.notMem_support_iff` `zero_smul` `Finset.subset_union_right` `Mathlib.Tactic.Contrapose.contrapose₂`
`linearIndependent_iff_eq_zero_of_smul_mem_span` 📖	mathematical	—	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`LinearIndependent.eq_zero_of_smul_mem_span` `linearIndependent_iff` `Finsupp.ext` `Finsupp.mem_span_image_iff_linearCombination` `Finsupp.mem_supported'` `Set.mem_diff` `Set.mem_univ` `Set.eq_of_mem_singleton` `Finsupp.single_eq_same` `sub_self` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Finsupp.linearCombination_single` `sub_zero`
`linearIndependent_iff_finset_linearIndependent` 📖	mathematical	—	`LinearIndependent` `Finset` `SetLike.instMembership` `Finset.instSetLike`	—	`LinearIndependent.comp` `Subtype.val_injective` `linearIndependent_iff'ₛ` `Fintype.linearIndependent_iffₛ` `Finset.sum_coe_sort`
`linearIndependent_iff_injective_finsuppLinearCombination` 📖	mathematical	—	`LinearIndependent` `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`	—	—
`linearIndependent_iff_injective_fintypeLinearCombination` 📖	mathematical	—	`LinearIndependent` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `Fintype.linearCombination`	—	`RingHomInvPair.ids` `Finite.of_fintype` `RingHomCompTriple.ids`
`linearIndependent_iff_ker` 📖	mathematical	—	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.ker` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `RingHom.id` `Finsupp.linearCombination` `Bot.bot` `Submodule` `Submodule.instBot`	—	`LinearMap.ker_eq_bot`
`linearIndependent_iff_notMem_span` 📖	mathematical	—	`LinearIndependent` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.image` `Set` `Set.instSDiff` `Set.univ` `Set.instSingletonSet`	—	`linearIndependent_iff_eq_zero_of_smul_mem_span` `one_ne_zero` `NeZero.one` `DivisionRing.toNontrivial` `one_smul` `Submodule.smul_mem_iff` `IsScalarTower.left`
`linearIndependent_iffₒₛ` 📖	mathematical	—	`LinearIndependent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`linearIndependent_iff'ₛ` `Disjoint.notMem_of_mem_left_finset` `Finset.sum_congr` `ite_smul` `zero_smul` `Finset.sum_ite_mem` `Finset.union_inter_cancel_left` `Finset.union_inter_cancel_right` `Finset.mem_union_left` `Disjoint.notMem_of_mem_right_finset` `Finset.mem_union_right` `LE.le.antisymm'` `CanonicallyOrderedAdd.toOrderedSub` `LE.le.not_gt` `add_right_cancel_iff` `IsCancelAdd.toIsRightCancelAdd` `add_assoc` `Finset.sum_add_distrib` `add_left_comm` `Finset.sum_filter_add_sum_filter_not` `Finset.filter.congr_simp` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `CanonicallyOrderedAdd.toAddLeftMono` `LT.lt.not_ge` `LT.lt.le` `LE.le.antisymm` `not_le`
`linearIndependent_iffₛ` 📖	mathematical	—	`LinearIndependent`	—	—
`linearIndependent_of_subsingleton` 📖	mathematical	—	`LinearIndependent`	—	`linearIndependent_iffₛ` `Unique.instSubsingleton`
`linearIndependent_restrict_iff` 📖	mathematical	—	`LinearIndependent` `Set.Elem` `Set.restrict` `LinearIndepOn`	—	—
`linearIndependent_set_coe_iff` 📖	mathematical	—	`LinearIndependent` `Set.Elem` `Set` `Set.instMembership` `LinearIndepOn`	—	—
`linearIndependent_subsingleton_iff` 📖	mathematical	—	`LinearIndependent` `IsEmpty`	—	`linearIndependent_zero_iff`
`linearIndependent_subtype_iff` 📖	mathematical	—	`LinearIndependent` `Set` `Set.instMembership` `LinearIndepOn`	—	—
`linearIndependent_zero_iff` 📖	mathematical	—	`LinearIndependent` `Pi.instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `IsEmpty`	—	`not_nonempty_iff` `LinearIndependent.ne_zero` `linearIndependent_empty_type`
`not_linearIndepOn_finset_iff` 📖	mathematical	—	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.sum` `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` `Finset.instMembership`	—	`Iff.not` `linearIndepOn_finset_iff`
`not_linearIndepOn_finset_iffₒₛ` 📖	mathematical	—	`LinearIndepOn` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.instHasSubset` `Finset.sum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Finset.instSDiff` `Finset.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Finset.sdiff_subset` `Finset.sum_congr` `Finset.sdiff_sdiff_eq_self` `Finset.mem_sdiff`
`not_linearIndepOn_finset_iffₛ` 📖	mathematical	—	`LinearIndepOn` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.sum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Finset.instMembership`	—	`Iff.not` `linearIndepOn_finset_iffₛ`
`not_linearIndependent_iff` 📖	mathematical	—	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Finset.sum` `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` `Finset` `Finset.instMembership`	—	`linearIndependent_iff'`
`not_linearIndependent_iffₒₛ` 📖	mathematical	—	`LinearIndependent` `Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `Finset.sum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Finset.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Mathlib.Tactic.Push.not_forall_eq` `Mathlib.Tactic.Push.not_and_or_eq` `Disjoint.symm`
`not_linearIndependent_iffₛ` 📖	mathematical	—	`LinearIndependent` `Finset.sum` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Finset` `Finset.instMembership`	—	`linearIndependent_iff'ₛ`

---

← Back to Index