Lemmas

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

Statistics

Metric	Count
Definitions `extend`, `equiv_linearIndependent`	2
Theorems `linearIndependent_iff'`, `linearIndependent_iff'ₛ`, `extend_subset`, `id_insert`, `id_insert'`, `image_subset_span_image_extend`, `insert`, `insert'`, `linearIndepOn_extend`, `mem_span_iff`, `mem_span_iff_id`, `notMem_span_iff`, `notMem_span_iff_id`, `pair_iff`, `span_extend_eq_span`, `span_image_extend_eq_span_image`, `subset_extend`, `subset_span_extend`, `eq_of_pair`, `eq_zero_of_pair`, `eq_zero_of_pair'`, `fin_cons`, `iSupIndep_span_singleton`, `inl_union_inr`, `isCompl_span_image`, `of_pairwise_dual_eq_zero_one`, `option`, `pair_add_left_iff`, `pair_add_right_iff`, `pair_add_smul_add_smul_iff`, `pair_add_smul_left_iff`, `pair_add_smul_right_iff`, `pair_iff`, `pair_iff'`, `pair_iffₛ`, `pair_neg_left_iff`, `pair_neg_right_iff`, `pair_smul_iff`, `pair_symm_iff`, `bijective_of_linearIndependent_of_span_eq_top`, `iSupIndep_map`, `injective_of_linearIndependent`, `codisjoint_span_image_of_codisjoint`, `exists_finite_card_le_of_finite_of_linearIndependent_of_span`, `exists_linearIndepOn_extension`, `exists_linearIndepOn_id_extension`, `exists_linearIndependent`, `exists_linearIndependent'`, `exists_maximal_linearIndepOn`, `exists_maximal_linearIndepOn'`, `exists_of_linearIndepOn_of_finite_span`, `iSupIndep_range_lsingle`, `linearIndepOn_biUnion_of_directed`, `linearIndepOn_iUnion_of_directed`, `linearIndepOn_id_iUnion_finite`, `linearIndepOn_id_insert`, `linearIndepOn_id_insert_iff`, `linearIndepOn_id_pair`, `linearIndepOn_insert`, `linearIndepOn_insert_iff`, `linearIndepOn_pair_iff`, `linearIndepOn_sUnion_of_directed`, `linearIndependent_algHom_toLinearMap`, `linearIndependent_algHom_toLinearMap'`, `linearIndependent_fin2`, `linearIndependent_fin_cons`, `linearIndependent_fin_snoc`, `linearIndependent_fin_succ`, `linearIndependent_fin_succ'`, `linearIndependent_iUnion_finite`, `linearIndependent_inl_union_inr'`, `linearIndependent_option`, `linearIndependent_option'`, `mem_span_insert_exchange`	74
Total	76

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`linearIndependent_iff'` 📖	mathematical	—	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.ker` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Pi.module` `Semiring.toModule` `RingHom.id` `Semiring.toNonAssocSemiring` `DFunLike.coe` `LinearEquiv` `Nat.instSemiring` `RingHomInvPair.ids` `LinearMap` `LinearMap.addCommMonoid` `LinearMap.module` `AddCommMonoid.toNatModule` `AddMonoid.nat_smulCommClass'` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearMap.lsum` `LinearMap.smulRight` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `LinearMap.id` `Bot.bot` `Submodule` `Submodule.instBot`	—	`RingHomInvPair.ids` `AddMonoid.nat_smulCommClass'` `IsScalarTower.left` `RingHomCompTriple.ids` `LinearMap.coe_sum` `Finset.sum_congr` `Finset.sum_apply`
`linearIndependent_iff'ₛ` 📖	mathematical	—	`LinearIndependent` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.module` `Semiring.toModule` `LinearMap.instFunLike` `LinearEquiv` `Nat.instSemiring` `RingHomInvPair.ids` `LinearMap.addCommMonoid` `LinearMap.module` `AddCommMonoid.toNatModule` `AddMonoid.nat_smulCommClass'` `AddCommMonoid.toAddMonoid` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearMap.lsum` `LinearMap.smulRight` `IsScalarTower.left` `DistribMulAction.toMulAction` `LinearMap.id`	—	`RingHomInvPair.ids` `AddMonoid.nat_smulCommClass'` `IsScalarTower.left` `RingHomCompTriple.ids` `LinearMap.coe_sum` `Finset.sum_congr` `Finset.sum_apply`

LinearIndepOn

Definitions

Name	Category	Theorems
`extend` 📖	CompOp	20 math math: `span_image_extend_eq_span_image`, `Module.Basis.coe_extendLe`, `Module.Basis.ofSpan_subset`, `extend_subset`, `Module.Basis.extendLe_subset`, `Module.Basis.range_extendLe`, `Module.Basis.subset_extendLe`, `subset_span_extend`, `Module.Basis.range_extend`, `Module.Basis.extend_apply_self`, `Module.Basis.range_ofSpan`, `span_extend_eq_span`, `image_subset_span_image_extend`, `subset_extend`, `linearIndepOn_extend`, `Module.Basis.ofSpan_apply_self`, `Module.Basis.extendLe_apply_self`, `Module.Basis.subset_extend`, `Module.Basis.coe_extend`, `Module.Basis.coe_ofSpan`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extend_subset` 📖	mathematical	`LinearIndepOn` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instHasSubset`	`extend`	—	`exists_linearIndepOn_extension`
`id_insert` 📖	mathematical	`LinearIndepOn` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span`	`Set` `Set.instInsert`	—	`insert` `Set.image_id`
`id_insert'` 📖	mathematical	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Set` `Set.instInsert`	—	`insert'` `Set.image_congr` `Set.image_id'`
`image_subset_span_image_extend` 📖	mathematical	`LinearIndepOn` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instHasSubset`	`Set.image` `SetLike.coe` `Submodule` `Submodule.setLike` `Submodule.span` `extend`	—	`exists_linearIndepOn_extension`
`insert` 📖	mathematical	`LinearIndepOn` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.image`	`Set` `Set.instInsert`	—	`Set.union_singleton` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `union` `singleton` `DivisionRing.isDomain` `DivisionSemiring.to_moduleIsTorsionFree` `Set.image_singleton` `Submodule.disjoint_span_singleton'`
`insert'` 📖	mathematical	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Set` `Set.instInsert`	—	`Set.union_singleton` `union` `singleton'` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `Set.image_singleton` `zero_smul`
`linearIndepOn_extend` 📖	mathematical	`LinearIndepOn` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instHasSubset`	`extend`	—	`exists_linearIndepOn_extension`
`mem_span_iff` 📖	mathematical	`LinearIndepOn` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	`Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.image` `Set` `Set.instMembership`	—	`Submodule.subset_span` `Set.mem_image_of_mem`
`mem_span_iff_id` 📖	mathematical	`LinearIndepOn` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	`Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set` `Set.instMembership`	—	`Set.image_congr` `Set.image_id'` `mem_span_iff`
`notMem_span_iff` 📖	mathematical	`LinearIndepOn` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	`Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.image` `Set` `Set.instInsert` `Set.instMembership`	—	`mem_span_iff`
`notMem_span_iff_id` 📖	mathematical	`LinearIndepOn` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	`Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set` `Set.instInsert` `Set.instMembership`	—	`mem_span_iff_id`
`pair_iff` 📖	mathematical	—	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instInsert` `Set.instSingletonSet` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`linearIndepOn_iff''` `Finset.coe_insert` `Finset.coe_singleton` `Set.instReflSubset` `Pi.single_eq_of_ne` `add_zero` `Finset.sum_congr` `Pi.single_apply` `Finset.sum_insert` `Finset.sum_singleton` `zero_add` `Finset.sum_pair` `Finset.sum_subset` `zero_smul`
`span_extend_eq_span` 📖	mathematical	`LinearIndepOn` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instHasSubset`	`Submodule.span` `extend`	—	`le_antisymm` `Submodule.span_mono` `extend_subset` `Submodule.span_le` `subset_span_extend`
`span_image_extend_eq_span_image` 📖	mathematical	`LinearIndepOn` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instHasSubset`	`Submodule.span` `Set.image` `extend`	—	`le_antisymm` `Submodule.span_mono` `Set.image_mono` `extend_subset` `Submodule.span_le` `image_subset_span_image_extend`
`subset_extend` 📖	mathematical	`LinearIndepOn` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instHasSubset`	`extend`	—	`exists_linearIndepOn_extension`
`subset_span_extend` 📖	mathematical	`LinearIndepOn` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instHasSubset`	`SetLike.coe` `Submodule` `Submodule.setLike` `Submodule.span` `extend`	—	`Set.image_congr` `Set.image_id'` `image_subset_span_image_extend`

LinearIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_pair` 📖	—	`LinearIndependent` `Matrix.vecCons` `Matrix.vecEmpty` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—	`pair_iffₛ`
`eq_zero_of_pair` 📖	mathematical	`LinearIndependent` `Matrix.vecCons` `Matrix.vecEmpty` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `Finsupp.linearCombination_single` `Matrix.cons_val_fin_one` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `Finsupp.single_eq_same` `Finsupp.single_eq_of_ne` `zero_add` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `add_zero`
`eq_zero_of_pair'` 📖	mathematical	`LinearIndependent` `Matrix.vecCons` `Matrix.vecEmpty` `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`	—	`eq_of_pair` `zero_smul` `add_zero` `zero_add`
`fin_cons` 📖	mathematical	`LinearIndependent` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range`	`Fin.cons`	—	`linearIndependent_fin_cons`
`iSupIndep_span_singleton` 📖	mathematical	`LinearIndependent`	`iSupIndep` `Submodule` `Submodule.completeLattice` `Submodule.span` `Set` `Set.instSingletonSet`	—	`RingHomSurjective.ids` `Submodule.ext` `Finsupp.linearCombination_single` `LinearMap.iSupIndep_map` `iSupIndep_range_lsingle`
`inl_union_inr` 📖	mathematical	`LinearIndependent` `Set.Elem` `Set` `Set.instMembership`	`Set.instUnion` `Set.image` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `LinearMap.instFunLike` `LinearMap.inl` `LinearMap.inr`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `ne_zero` `linearIndependent_equiv'` `linearIndependent_inl_union_inr'`
`isCompl_span_image` 📖	mathematical	`LinearIndependent` `Submodule.span` `Set.range` `Top.top` `Submodule` `Submodule.instTop` `IsCompl` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Set.instBoundedOrder`	`Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `Set.image`	—	`disjoint_span_image` `IsCompl.disjoint` `Submodule.codisjoint_span_image_of_codisjoint` `IsCompl.codisjoint`
`of_pairwise_dual_eq_zero_one` 📖	mathematical	`Pairwise` `DFunLike.coe` `Module.Dual` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.id` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	`LinearIndependent`	—	`linearIndependent_iff'` `MulZeroClass.mul_zero` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Finset.sum_congr` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `Finset.sum_eq_single` `mul_one` `map_zero` `AddMonoidHomClass.toZeroHomClass`
`option` 📖	mathematical	`LinearIndependent` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range`	`Option.casesOn'`	—	`linearIndependent_option'`
`pair_add_left_iff` 📖	mathematical	—	`LinearIndependent` `Matrix.vecCons` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `Matrix.vecEmpty` `Ring.toSemiring`	—	`pair_symm_iff` `add_comm` `pair_add_right_iff`
`pair_add_right_iff` 📖	mathematical	—	`LinearIndependent` `Matrix.vecCons` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `Matrix.vecEmpty` `Ring.toSemiring`	—	`sub_smul` `smul_add` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Abel.zero_termg` `sub_zero` `neg_add_cancel_left`
`pair_add_smul_add_smul_iff` 📖	mathematical	—	`LinearIndependent` `Matrix.vecCons` `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` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `Matrix.vecEmpty` `Ring.toSemiring`	—	`eq_or_ne` `pair_iff` `Mathlib.Tactic.Push.not_forall_eq` `Mathlib.Tactic.Push.not_and_eq` `zero_smul` `add_zero` `smul_zero` `NeZero.one` `smul_assoc` `one_smul` `neg_smul` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `Mathlib.Tactic.Module.NF.neg_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval₂` `zero_add` `Mathlib.Tactic.Module.NF.zero_eq_eval` `Mathlib.Tactic.Module.NF.eq_cons_const` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `IsDomain.toIsCancelMulZero` `smul_add` `smul_smul` `mul_comm` `Mathlib.Tactic.Module.NF.add_eq_eval₁` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Contrapose.contrapose₂` `Fintype.complete` `Mathlib.Tactic.Module.NF.eq_cons_cons` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Module.NF.eq_const_cons` `Matrix.cons_val_fin_one` `Mathlib.Tactic.Module.NF.add_eq_eval₃` `Mathlib.Tactic.Ring.add_pf_add_gt` `mul_neg` `neg_mul` `neg_neg` `pair_smul_iff` `sub_ne_zero_of_ne`
`pair_add_smul_left_iff` 📖	mathematical	—	`LinearIndependent` `Matrix.vecCons` `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` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `Matrix.vecEmpty` `Ring.toSemiring`	—	`subsingleton_or_nontrivial` `zero_smul` `add_zero` `Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `one_smul` `zero_add` `mul_one` `MulZeroClass.mul_zero` `NeZero.one` `pair_add_smul_add_smul_iff`
`pair_add_smul_right_iff` 📖	mathematical	—	`LinearIndependent` `Matrix.vecCons` `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` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `Matrix.vecEmpty` `Ring.toSemiring`	—	`subsingleton_or_nontrivial` `zero_smul` `zero_add` `Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `one_smul` `add_zero` `mul_one` `MulZeroClass.zero_mul` `NeZero.one` `pair_add_smul_add_smul_iff`
`pair_iff` 📖	mathematical	—	`LinearIndependent` `Matrix.vecCons` `Matrix.vecEmpty` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`linearIndepOn_univ` `Finset.coe_univ` `Finset.coe_insert` `Finset.coe_singleton` `LinearIndepOn.pair_iff` `Matrix.cons_val_fin_one`
`pair_iff'` 📖	mathematical	—	`LinearIndependent` `Matrix.vecCons` `Matrix.vecEmpty` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	—	`linearIndepOn_univ` `Finset.coe_univ` `Finset.coe_insert` `Finset.coe_singleton` `linearIndepOn_pair_iff` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `Matrix.cons_val_fin_one`
`pair_iffₛ` 📖	mathematical	—	`LinearIndependent` `Matrix.vecCons` `Matrix.vecEmpty`	—	`Fin.sum_univ_two` `Matrix.cons_val_fin_one`
`pair_neg_left_iff` 📖	mathematical	—	`LinearIndependent` `Matrix.vecCons` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Matrix.vecEmpty` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`pair_iff` `smul_neg` `neg_smul` `neg_neg`
`pair_neg_right_iff` 📖	mathematical	—	`LinearIndependent` `Matrix.vecCons` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Matrix.vecEmpty` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`pair_symm_iff` `pair_neg_left_iff`
`pair_smul_iff` 📖	mathematical	—	`LinearIndependent` `Matrix.vecCons` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Matrix.vecEmpty` `Ring.toSemiring`	—	`SMulCommClass.smul_comm` `smul_add` `smul_zero` `smul_eq_zero_iff_right` `IsDomain.toIsCancelMulZero` `smul_assoc`
`pair_symm_iff` 📖	mathematical	—	`LinearIndependent` `Matrix.vecCons` `Matrix.vecEmpty` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`add_comm`

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijective_of_linearIndependent_of_span_eq_top` 📖	mathematical	`Submodule.span` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set.range` `Top.top` `Submodule` `Submodule.instTop` `LinearIndependent` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike`	`Function.Bijective`	—	`injective_of_linearIndependent` `RingHomSurjective.ids` `range_eq_top` `Submodule.map_top` `Submodule.map_span` `Set.range_comp`
`iSupIndep_map` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike` `iSupIndep` `Submodule` `Submodule.completeLattice`	`Submodule.map` `RingHomSurjective.ids`	—	`RingHomSurjective.ids` `iSup_congr_Prop` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass`
`injective_of_linearIndependent` 📖	—	`Submodule.span` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Set.range` `Top.top` `Submodule` `Submodule.instTop` `LinearIndependent` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike`	—	—	`injective_iff_map_eq_zero` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass` `Submodule.mem_top` `Finsupp.mem_span_range_iff_exists_finsupp` `linearIndependent_iff` `map_finsuppSum` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass`

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`codisjoint_span_image_of_codisjoint` 📖	mathematical	`span` `Set.range` `Top.top` `Submodule` `instTop` `Codisjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Set.instOrderTop`	`instPartialOrder` `instOrderTop` `Set.image`	—	`RingHomSurjective.ids` `Finsupp.span_image_eq_map_linearCombination` `codisjoint_map` `LinearMap.range_eq_top` `Finsupp.range_linearCombination` `Finsupp.codisjoint_supported_supported`

(root)

Definitions

Name	Category	Theorems
`equiv_linearIndependent` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_finite_card_le_of_finite_of_linearIndependent_of_span` 📖	mathematical	`LinearIndepOn` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instHasSubset` `SetLike.coe` `Submodule` `Submodule.setLike` `Submodule.span`	`Finset.card` `Set.Finite.toFinset`	—	`Set.Finite.coe_toFinset` `exists_of_linearIndepOn_of_finite_span` `Set.Finite.subset` `Finset.finite_toSet` `Finset.card_le_card` `Finset.coe_subset`
`exists_linearIndepOn_extension` 📖	mathematical	`LinearIndepOn` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instHasSubset`	`Set.image` `SetLike.coe` `Submodule` `Submodule.setLike` `Submodule.span`	—	`zorn_subset_nonempty` `Set.sUnion_subset` `linearIndepOn_sUnion_of_directed` `IsChain.directedOn` `Set.instReflSubset` `Set.subset_sUnion_of_mem` `Maximal.prop` `by_contra` `Submodule.subset_span` `Set.mem_image_of_mem` `Maximal.mem_of_prop_insert` `Set.insert_subset` `LinearIndepOn.insert`
`exists_linearIndepOn_id_extension` 📖	mathematical	`LinearIndepOn` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instHasSubset`	`SetLike.coe` `Submodule` `Submodule.setLike` `Submodule.span`	—	`Set.image_congr` `Set.image_id'` `exists_linearIndepOn_extension`
`exists_linearIndependent` 📖	mathematical	—	`Set` `Set.instHasSubset` `Submodule.span` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `LinearIndependent` `Set.instMembership`	—	`exists_linearIndepOn_id_extension` `linearIndependent_empty` `Set.empty_subset` `Submodule.span_eq_of_le` `Submodule.span_mono`
`exists_linearIndependent'` 📖	mathematical	—	`Submodule.span` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Set.range` `LinearIndependent`	—	`exists_linearIndependent` `Subtype.val_injective` `Set.ext` `LinearIndependent.comp`
`exists_maximal_linearIndepOn` 📖	mathematical	—	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.image` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`exists_maximal_linearIndepOn'` `Set.union_singleton` `linearDepOn_iff` `Mathlib.Tactic.Contrapose.contrapose₃` `Finsupp.mem_support_iff` `add_eq_zero_iff_eq_neg` `Finset.sum_insert` `Finset.notMem_erase` `Finset.insert_erase` `NegMemClass.neg_mem` `AddSubgroupClass.toNegMemClass` `Submodule.addSubgroupClass` `sum_mem` `Submodule.addSubmonoidClass` `Submodule.smul_mem` `Submodule.subset_span` `Finset.erase_subset` `Finset.ne_of_mem_erase`
`exists_maximal_linearIndepOn'` 📖	mathematical	—	`LinearIndepOn`	—	`linearIndepOn_iffₛ` `Set.eq_empty_or_nonempty` `Set.iUnion_congr_Prop` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `Finsupp.supported_empty` `DirectedOn.exists_mem_subset_of_finset_subset_biUnion` `IsChain.directedOn` `Set.Subset.refl` `Finset.coe_union` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.subset_union_left` `Set.subset_union_right` `Set.Subset.trans` `exists_maximal_of_chains_bounded` `Set.subset_biUnion_of_mem` `Set.Subset.antisymm`
`exists_of_linearIndepOn_of_finite_span` 📖	mathematical	`LinearIndepOn` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instHasSubset` `SetLike.coe` `Submodule` `Submodule.setLike` `Submodule.span` `Finset` `Finset.instSetLike`	`Set.instUnion` `Finset.card`	—	`Finset.induction_on` `eq_of_linearIndepOn_id_of_span_subtype` `DivisionRing.toNontrivial` `Finset.union_empty` `Finset.coe_empty` `Set.union_empty` `Set.instReflSubset` `Finset.mem_insert_self` `Set.eq_empty_of_subset_empty` `Set.Subset.trans` `Finset.coe_insert` `le_of_eq` `Classical.by_cases` `Set.union_insert` `Set.insert_subset_insert` `Finset.card_insert_of_notMem` `Finset.union_insert` `Set.not_subset` `Submodule.subset_span` `Submodule.span_mono` `Finset.coe_union` `Submodule.span_union` `mem_span_insert_exchange` `Finset.insert_union` `Submodule.span_insert_eq_span` `Set.union_subset_union` `Set.Subset.refl` `Finset.ext` `Finset.coe_filter`
`iSupIndep_range_lsingle` 📖	mathematical	—	`iSupIndep` `Submodule` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddCommMonoid` `Finsupp.module` `Submodule.completeLattice` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Finsupp.lsingle`	—	`RingHomSurjective.ids` `disjoint_iff_inf_le` `iSup₂_le` `Finsupp.single_eq_of_ne'` `Finsupp.mem_supported` `Finsupp.single_eq_same` `Finsupp.single_zero` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass`
`linearIndepOn_biUnion_of_directed` 📖	mathematical	`DirectedOn` `Order.Preimage` `Set` `Set.instHasSubset` `LinearIndepOn`	`Set.iUnion` `Set.instMembership`	—	`Set.biUnion_eq_iUnion` `linearIndepOn_iUnion_of_directed` `directed_comp` `DirectedOn.directed_val`
`linearIndepOn_iUnion_of_directed` 📖	mathematical	`Directed` `Set` `Set.instHasSubset` `LinearIndepOn`	`Set.iUnion`	—	`linearIndepOn_of_finite` `Set.finite_subset_iUnion` `Directed.finset_le` `Set.instIsTransSubset` `LinearIndepOn.mono` `Set.Subset.trans` `Set.iUnion₂_subset` `Set.Finite.mem_toFinset` `linearIndepOn_empty`
`linearIndepOn_id_iUnion_finite` 📖	mathematical	`LinearIndepOn` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Disjoint` `Submodule` `Submodule.instPartialOrder` `Submodule.instOrderBot` `Submodule.span` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Set` `Set.instMembership`	`Set.iUnion`	—	`Set.iUnion_eq_iUnion_finset` `linearIndepOn_iUnion_of_directed` `directed_of_isDirected_le` `Finset.isDirected_le` `Set.iUnion_mono` `Set.iUnion_subset_iUnion_const` `Finset.induction_on` `Set.iUnion_congr_Prop` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `Finset.set_biUnion_insert` `LinearIndepOn.id_union` `Submodule.span_iUnion₂` `Finset.finite_toSet`
`linearIndepOn_id_insert` 📖	mathematical	`Set` `Set.instMembership`	`LinearIndepOn` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Set.instInsert` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span`	—	`linearIndepOn_insert` `Set.image_congr` `Set.image_id'`
`linearIndepOn_id_insert_iff` 📖	mathematical	—	`LinearIndepOn` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instInsert` `Set.instMembership`	—	`Set.image_congr` `Set.image_id'` `linearIndepOn_insert_iff`
`linearIndepOn_id_pair` 📖	mathematical	—	`LinearIndepOn` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instInsert` `Set.instSingletonSet`	—	`Set.pair_comm` `LinearIndepOn.id_insert` `LinearIndepOn.singleton` `DivisionRing.isDomain` `DivisionSemiring.to_moduleIsTorsionFree`
`linearIndepOn_insert` 📖	mathematical	`Set` `Set.instMembership`	`LinearIndepOn` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Set.instInsert` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.image`	—	`LinearIndepOn.eq_1` `linearIndependent_equiv` `linearIndependent_option` `Set.range_comp'` `Subtype.range_coe_subtype`
`linearIndepOn_insert_iff` 📖	mathematical	—	`LinearIndepOn` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instInsert` `Set.instMembership`	—	`Set.insert_eq_of_mem` `linearIndepOn_insert`
`linearIndepOn_pair_iff` 📖	mathematical	—	`LinearIndepOn` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Set` `Set.instInsert` `Set.instSingletonSet`	—	`Set.pair_comm` `DivisionSemiring.to_moduleIsTorsionFree` `IsDomain.toIsCancelMulZero` `DivisionRing.isDomain` `Set.image_singleton` `linearIndepOn_insert`
`linearIndepOn_sUnion_of_directed` 📖	mathematical	`DirectedOn` `Set` `Set.instHasSubset` `LinearIndepOn`	`Set.sUnion`	—	`Set.sUnion_eq_iUnion` `linearIndepOn_iUnion_of_directed` `DirectedOn.directed_val`
`linearIndependent_algHom_toLinearMap` 📖	mathematical	—	`LinearIndependent` `AlgHom` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `AlgHom.toLinearMap` `LinearMap.addCommMonoid` `LinearMap.module` `Semiring.toModule` `Algebra.to_smulCommClass`	—	`LinearIndependent.of_comp` `Algebra.to_smulCommClass` `LinearIndependent.comp` `linearIndependent_monoidHom` `AlgHom.ext` `DFunLike.congr_fun`
`linearIndependent_algHom_toLinearMap'` 📖	mathematical	—	`LinearIndependent` `AlgHom` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `AlgHom.toLinearMap` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing`	—	`LinearIndependent.restrict_scalars'` `smulCommClass_self` `Algebra.to_smulCommClass` `LinearMap.instIsScalarTower` `IsScalarTower.right` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `linearIndependent_algHom_toLinearMap`
`linearIndependent_fin2` 📖	mathematical	—	`LinearIndependent` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	—	`linearIndependent_fin_succ` `linearIndependent_unique_iff` `DivisionRing.isDomain` `DivisionSemiring.to_moduleIsTorsionFree` `Set.range_unique` `Submodule.mem_span_singleton`
`linearIndependent_fin_cons` 📖	mathematical	—	`LinearIndependent` `Fin.cons` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range`	—	`linearIndependent_equiv` `linearIndependent_option`
`linearIndependent_fin_snoc` 📖	mathematical	—	`LinearIndependent` `Fin.snoc` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range`	—	`Fin.snoc_eq_cons_rotate` `linearIndependent_equiv` `linearIndependent_fin_cons`
`linearIndependent_fin_succ` 📖	mathematical	—	`LinearIndependent` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Fin.tail` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range`	—	`linearIndependent_fin_cons` `Fin.cons_self_tail`
`linearIndependent_fin_succ'` 📖	mathematical	—	`LinearIndependent` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Fin.init` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range`	—	`linearIndependent_fin_snoc` `Fin.snoc_init_self`
`linearIndependent_iUnion_finite` 📖	—	`LinearIndependent` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Disjoint` `Submodule` `Submodule.instPartialOrder` `Submodule.instOrderBot` `Submodule.span` `Set.range` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Set` `Set.instMembership`	—	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `LinearIndependent.of_linearIndepOn_id_range` `Sigma.eq` `LinearIndependent.injective` `Submodule.disjoint_def` `Set.finite_singleton` `Set.eq_of_mem_singleton` `Submodule.subset_span` `Set.mem_range_self` `iSup_singleton` `LinearIndependent.ne_zero` `Set.range_sigma_eq_iUnion_range` `linearIndepOn_id_iUnion_finite` `LinearIndependent.linearIndepOn_id`
`linearIndependent_inl_union_inr'` 📖	mathematical	`LinearIndependent`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `LinearMap.instFunLike` `LinearMap.inl` `LinearMap.inr`	—	`RingHomCompTriple.ids` `RingHomInvPair.ids` `Finsupp.lhom_ext'` `LinearMap.ext_ring` `Finsupp.linearCombination_single` `one_smul` `Finsupp.comapDomain_single` `Finsupp.linearCombination_comapDomain` `Finset.sum_congr` `Finset.preimage_inr` `Finsupp.single_eq_of_ne` `zero_smul` `Finset.sum_const_zero` `Finset.preimage_inl` `LinearIndependent.eq_1`
`linearIndependent_option` 📖	mathematical	—	`LinearIndependent` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range`	—	`Option.casesOn'_none_coe`
`linearIndependent_option'` 📖	mathematical	—	`LinearIndependent` `Option.casesOn'` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.range`	—	`linearIndependent_equiv` `linearIndependent_sum` `Set.range_unique` `linearIndependent_unique_iff` `DivisionRing.isDomain` `DivisionSemiring.to_moduleIsTorsionFree` `Submodule.disjoint_span_singleton` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass`
`mem_span_insert_exchange` 📖	—	`Submodule` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set` `Set.instInsert`	—	—	`Submodule.smul_mem` `zero_smul` `zero_add` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `Mathlib.Tactic.Module.NF.add_eq_eval₁` `Mathlib.Tactic.Module.NF.add_eq_eval₂` `Mathlib.Tactic.Module.NF.eq_cons_cons` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `mul_one` `inv_mul_cancel₀` `Mathlib.Tactic.Module.NF.eq_const_cons` `add_neg_cancel`

---

← Back to Index