Independent

📁 Source: Mathlib/LinearAlgebra/AffineSpace/Independent.lean

Statistics

Metric	Count
Definitions `AffineIndependent`, `Independent`	2
Theorems `affineIndependent_iff`, `affineIndependent_set_of_eq_iff`, `affineCombination_eq_iff_eq`, `affineCombination_eq_lineMap_iff_weight_lineMap`, `affineIndependent_of_notMem_span`, `affineIndependent_update_of_notMem_affineSpan`, `affineSpan_disjoint_of_disjoint`, `comm_left`, `comm_right`, `comp_embedding`, `eq_of_sum_eq_sum`, `eq_of_sum_eq_sum_subtype`, `eq_zero_of_affineCombination_mem_affineSpan`, `eq_zero_of_sum_eq_zero`, `eq_zero_of_sum_eq_zero_subtype`, `exists_mem_inter_of_exists_mem_inter_affineSpan`, `indicator_eq_of_affineCombination_eq`, `indicator_extend_eq_of_affineCombination_comp_embedding_eq`, `indicator_extend_eq_of_affineCombination_comp_embedding_eq_of_fintype`, `inf_affineSpan_eq_affineSpan_inter`, `injective`, `injective_affineSpan_image`, `map'`, `mem_affineSpan_iff`, `mono`, `notMem_affineSpan_diff`, `of_comp`, `of_set_of_injective`, `of_smul`, `of_vadd`, `range`, `reverse_of_three`, `smul`, `subtype`, `units_lineMap`, `vadd`, `vectorSpan_image_eq_iff`, `affineIndependent_iff`, `affineCombination_mem_affineSpan_pair`, `affineIndependent_def`, `affineIndependent_equiv`, `affineIndependent_iff`, `affineIndependent_iff_eq_of_fintype_affineCombination_eq`, `affineIndependent_iff_indicator_eq_of_affineCombination_eq`, `affineIndependent_iff_linearIndependent_vsub`, `affineIndependent_iff_of_fintype`, `affineIndependent_of_ne`, `affineIndependent_of_ne_of_mem_of_mem_of_notMem`, `affineIndependent_of_ne_of_mem_of_notMem_of_mem`, `affineIndependent_of_ne_of_notMem_of_mem_of_mem`, `affineIndependent_of_subsingleton`, `affineIndependent_set_iff_linearIndependent_vsub`, `affineIndependent_smul`, `affineIndependent_vadd`, `exists_affineIndependent`, `exists_nontrivial_relation_sum_zero_of_not_affine_ind`, `exists_subset_affineIndependent_affineSpan_eq_top`, `linearIndependent_set_iff_affineIndependent_vadd_union_singleton`, `sign_eq_of_affineCombination_mem_affineSpan_pair`, `sign_eq_of_affineCombination_mem_affineSpan_single_lineMap`, `weightedVSub_mem_vectorSpan_pair`	61
Total	63

AffineEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`affineIndependent_iff` 📖	mathematical	—	`AffineIndependent` `DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike`	—	`AffineMap.affineIndependent_iff` `Equiv.injective`
`affineIndependent_set_of_eq_iff` 📖	mathematical	—	`AffineIndependent` `Set` `Set.instMembership` `Set.image` `DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike`	—	`affineIndependent_iff`

AffineIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`affineCombination_eq_iff_eq` 📖	mathematical	`AffineIndependent` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	`DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination`	—	`indicator_eq_of_affineCombination_eq` `Set.indicator_of_mem` `Finset.affineCombination_congr`
`affineCombination_eq_lineMap_iff_weight_lineMap` 📖	mathematical	`AffineIndependent` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	`DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `AffineMap.lineMap`	—	`AffineMap.apply_lineMap` `affineCombination_eq_iff_eq` `Finset.sum_congr` `Finset.sum_add_distrib` `Finset.sum_sub_distrib` `sub_self` `MulZeroClass.mul_zero` `zero_add`
`affineIndependent_of_notMem_span` 📖	—	`AffineIndependent` `DivisionRing.toRing` `AffineSubspace` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set.image` `setOf`	—	—	`neg_smul` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `smul_zero` `neg_zero` `Finset.sum_congr` `Finset.sum_neg_distrib` `MulZeroClass.mul_zero` `inv_mul_cancel₀` `Finset.sum_subtype_eq_sum_filter` `Finset.filter.congr_simp` `Finset.filter_eq'` `Finset.sum_singleton` `Finset.sum_filter_add_sum_filter_not` `Finset.affineCombination_eq_of_weightedVSub_eq_zero_of_eq_neg_one` `Subtype.range_coe` `Set.range_comp` `Finset.affineCombination_subtype_eq_filter` `affineCombination_mem_affineSpan` `DivisionRing.toNontrivial` `Finset.sum_filter_of_ne` `not_and_or` `Finset.weightedVSub_subtype_eq_filter` `Finset.weightedVSub_filter_of_ne` `Finset.mem_subtype`
`affineIndependent_update_of_notMem_affineSpan` 📖	mathematical	`AffineIndependent` `DivisionRing.toRing` `AffineSubspace` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set.image` `setOf`	`Function.update`	—	`Function.update_of_ne` `Set.image_congr` `subtype` `affineIndependent_of_notMem_span` `Function.update_self`
`affineSpan_disjoint_of_disjoint` 📖	mathematical	`AffineIndependent` `Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`SetLike.coe` `AffineSubspace` `AffineSubspace.instSetLike` `affineSpan` `Set.image`	—	`Set.disjoint_left` `exists_mem_inter_of_exists_mem_inter_affineSpan` `Set.disjoint_iff`
`comm_left` 📖	—	`AffineIndependent` `Matrix.vecCons` `Matrix.vecEmpty`	—	—	`affineIndependent_equiv` `Fintype.complete`
`comm_right` 📖	—	`AffineIndependent` `Matrix.vecCons` `Matrix.vecEmpty`	—	—	`affineIndependent_equiv` `Fintype.complete`
`comp_embedding` 📖	mathematical	`AffineIndependent`	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	—	`Function.Embedding.injective` `Finset.sum_map` `Finset.sum_congr` `Finset.weightedVSub_map` `Finset.mem_map'`
`eq_of_sum_eq_sum` 📖	—	`AffineIndependent` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `Finset` `Finset.instMembership`	—	—	`sub_eq_zero` `eq_zero_of_sum_eq_zero` `Finset.sum_congr` `Finset.sum_sub_distrib` `sub_smul`
`eq_of_sum_eq_sum_subtype` 📖	—	`AffineIndependent` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `Finset.instMembership`	—	—	`sub_eq_zero` `eq_zero_of_sum_eq_zero_subtype` `Finset.sum_congr` `Finset.sum_sub_distrib` `sub_smul`
`eq_zero_of_affineCombination_mem_affineSpan` 📖	mathematical	`AffineIndependent` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `AffineSubspace` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set.image` `DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination` `Finset` `Finset.instMembership` `Set` `Set.instMembership`	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`eq_affineCombination_of_mem_affineSpan_image` `indicator_eq_of_affineCombination_eq` `Set.indicator_of_notMem` `Set.notMem_subset` `Set.indicator_apply_eq_zero` `Finset.mem_coe`
`eq_zero_of_sum_eq_zero` 📖	—	`AffineIndependent` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Finset` `Finset.instMembership`	—	—	`affineIndependent_iff`
`eq_zero_of_sum_eq_zero_subtype` 📖	—	`AffineIndependent` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Finset.instMembership`	—	—	`eq_zero_of_sum_eq_zero` `Finset.sum_attach` `Finset.mem_univ`
`exists_mem_inter_of_exists_mem_inter_affineSpan` 📖	mathematical	`AffineIndependent` `AffineSubspace` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set.image`	`Set` `Set.instMembership` `Set.instInter`	—	`Set.Nonempty.eq_1` `Set.not_nonempty_iff_eq_empty` `Set.image_empty` `AffineSubspace.span_empty` `inf_affineSpan_eq_affineSpan_inter`
`indicator_eq_of_affineCombination_eq` 📖	mathematical	`AffineIndependent` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination`	`Set.indicator` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`affineIndependent_iff_indicator_eq_of_affineCombination_eq`
`indicator_extend_eq_of_affineCombination_comp_embedding_eq` 📖	mathematical	`AffineIndependent` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination` `Function.Embedding` `Function.instFunLikeEmbedding`	`Set.indicator` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.map` `Function.extend` `Pi.instZero`	—	`Function.extend_comp` `Function.Embedding.injective` `indicator_eq_of_affineCombination_eq` `Finset.sum_map` `Finset.sum_congr` `Function.Injective.extend_apply` `Finset.affineCombination_map`
`indicator_extend_eq_of_affineCombination_comp_embedding_eq_of_fintype` 📖	mathematical	`AffineIndependent` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finset.univ` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination` `Function.Embedding` `Function.instFunLikeEmbedding`	`Set.indicator` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Set.range` `Function.extend` `Pi.instZero`	—	`Finset.coe_map` `Finset.coe_univ` `Set.image_univ` `Set.indicator_univ` `indicator_extend_eq_of_affineCombination_comp_embedding_eq`
`inf_affineSpan_eq_affineSpan_inter` 📖	mathematical	`AffineIndependent`	`AffineSubspace` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `AffineSubspace.instCompleteLattice` `affineSpan` `Set.image` `Set` `Set.instInter`	—	`AffineSubspace.ext` `Set.image_eq_range` `affineIndependent_iff_indicator_eq_of_affineCombination_eq` `Finset.sum_inter_add_sum_diff` `Finset.sum_eq_zero` `Set.indicator_of_mem` `Set.indicator_of_notMem` `add_zero` `Finset.affineCombination_indicator_subset` `Finset.inter_subset_left` `Finset.affineCombination_congr` `Finset.coe_inter` `Set.indicator_indicator` `Set.indicator_apply`
`injective` 📖	—	`AffineIndependent`	—	—	`LinearIndependent.ne_zero` `affineIndependent_iff_linearIndependent_vsub` `vsub_eq_zero_iff_eq`
`injective_affineSpan_image` 📖	mathematical	`AffineIndependent`	`Set` `AffineSubspace` `affineSpan` `Set.image`	—	`Function.not_injective_iff` `Set.ext` `mem_affineSpan_iff`
`map'` 📖	—	`AffineIndependent` `DFunLike.coe` `AffineMap` `AffineMap.instFunLike`	—	—	`isEmpty_or_nonempty` `affineIndependent_of_subsingleton` `IsEmpty.instSubsingleton` `affineIndependent_iff_linearIndependent_vsub` `AffineMap.linearMap_vsub` `LinearMap.ker_eq_bot` `AffineMap.linear_injective_iff` `LinearIndependent.map'`
`mem_affineSpan_iff` 📖	mathematical	`AffineIndependent`	`AffineSubspace` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set.image` `Set` `Set.instMembership`	—	`exists_mem_inter_of_exists_mem_inter_affineSpan` `mem_affineSpan` `Set.mem_image_of_mem` `Set.mem_singleton` `Set.inter_singleton_nonempty` `Set.nonempty_def`
`mono` 📖	—	`AffineIndependent` `Set.Elem` `Set` `Set.instMembership` `Set.instHasSubset`	—	—	`comp_embedding`
`notMem_affineSpan_diff` 📖	mathematical	`AffineIndependent`	`AffineSubspace` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set.image` `Set` `Set.instSDiff` `Set.instSingletonSet`	—	—
`of_comp` 📖	—	`AffineIndependent` `DFunLike.coe` `AffineMap` `AffineMap.instFunLike`	—	—	`isEmpty_or_nonempty` `affineIndependent_of_subsingleton` `IsEmpty.instSubsingleton` `affineIndependent_iff_linearIndependent_vsub` `LinearIndependent.of_comp` `AffineMap.linearMap_vsub`
`of_set_of_injective` 📖	—	`AffineIndependent` `Set.Elem` `Set.range` `Set` `Set.instMembership`	—	—	`comp_embedding` `Set.mem_range_self`
`of_smul` 📖	—	`AffineIndependent` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—	`affineIndependent_smul`
`of_vadd` 📖	—	`AffineIndependent` `HVAdd.hVAdd` `instHVAdd` `Function.hasVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	—	`affineIndependent_vadd`
`range` 📖	mathematical	`AffineIndependent`	`Set.Elem` `Set.range` `Set` `Set.instMembership`	—	`comp_embedding`
`reverse_of_three` 📖	—	`AffineIndependent` `Matrix.vecCons` `Matrix.vecEmpty`	—	—	`affineIndependent_equiv` `Fintype.complete`
`smul` 📖	mathematical	`AffineIndependent` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup`	`Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`affineIndependent_smul`
`subtype` 📖	mathematical	`AffineIndependent`	`Set.Elem` `Set` `Set.instMembership`	—	`comp_embedding`
`units_lineMap` 📖	mathematical	`AffineIndependent`	`DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `AffineMap.lineMap` `Units.val` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`affineIndependent_iff_linearIndependent_vsub` `AffineMap.lineMap_same` `AffineMap.lineMap_vsub_left` `LinearIndependent.units_smul`
`vadd` 📖	mathematical	`AffineIndependent`	`HVAdd.hVAdd` `instHVAdd` `Function.hasVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	`affineIndependent_vadd`
`vectorSpan_image_eq_iff` 📖	mathematical	`AffineIndependent`	`vectorSpan` `Set.image` `Set.Subsingleton`	—	`Set.subsingleton_of_image` `injective` `vectorSpan_eq_bot_iff_subsingleton` `vectorSpan_of_subsingleton` `Set.Subsingleton.image`

AffineMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`affineIndependent_iff` 📖	mathematical	`DFunLike.coe` `AffineMap` `instFunLike`	`AffineIndependent`	—	`AffineIndependent.of_comp` `AffineIndependent.map'`

Projectivization

Definitions

Name	Category	Theorems
`Independent` 📖	CompData	5 math math: `independent_iff_iSupIndep`, `independent_iff_not_dependent`, `independent_pair_iff_ne`, `dependent_iff_not_independent`, `independent_iff`

(root)

Definitions

Name	Category	Theorems
`AffineIndependent` 📖	MathDef	49 math math: `affineIndependent_of_ne_of_notMem_of_mem_of_mem`, `exists_affineIndependent`, `EuclideanGeometry.Cospherical.affineIndependent_of_mem_of_ne`, `affineIndependent_iff_not_collinear_set`, `affineIndependent_of_ne_of_mem_of_notMem_of_mem`, `IsOpen.exists_subset_affineIndependent_span_eq_top`, `finrank_vectorSpan_le_iff_not_affineIndependent`, `affineIndependent_equiv`, `Affine.Simplex.affineIndependent_points_update_centroid`, `affineIndependent_set_iff_linearIndependent_vsub`, `AffineBasis.affineIndependent_of_toMatrix_right_inv`, `collinear_iff_not_affineIndependent_of_ne`, `EuclideanGeometry.Cospherical.affineIndependent_of_ne`, `AffineBasis.ind`, `affineIndependent_iff_not_finrank_vectorSpan_le`, `affineIndependent_iff_indicator_eq_of_affineCombination_eq`, `eq_pos_convex_span_of_mem_convexHull`, `affineIndependent_iff`, `isOpen_setOf_affineIndependent`, `Geometry.SimplicialComplex.indep`, `EuclideanGeometry.OrthocentricSystem.affineIndependent`, `affineIndependent_smul`, `affineIndependent_iff_le_finrank_vectorSpan`, `EuclideanGeometry.oangle_ne_zero_and_ne_pi_iff_affineIndependent`, `EuclideanGeometry.Cospherical.affineIndependent`, `affineIndependent_iff_eq_of_fintype_affineCombination_eq`, `linearIndependent_set_iff_affineIndependent_vadd_union_singleton`, `affineIndependent_of_ne`, `affineIndependent_iff_affineIndependent_collinear_ne`, `affineIndependent_iff_not_collinear_of_ne`, `AffineEquiv.affineIndependent_set_of_eq_iff`, `AffineBasis.ind'`, `Caratheodory.affineIndependent_minCardFinsetOfMemConvexHull`, `AffineBasis.isUnit_toMatrix_iff`, `affineIndependent_iff_not_collinear`, `affineIndependent_of_subsingleton`, `collinear_iff_not_affineIndependent_set`, `Affine.Simplex.independent`, `affineIndependent_iff_linearIndependent_vsub`, `affineIndependent_iff_finrank_vectorSpan_eq`, `convexHull_eq_union`, `affineIndependent_of_ne_of_mem_of_mem_of_notMem`, `affineIndependent_def`, `affineIndependent_iff_of_fintype`, `EuclideanGeometry.affineIndependent_iff_of_two_zsmul_oangle_eq`, `AffineEquiv.affineIndependent_iff`, `collinear_iff_not_affineIndependent`, `affineIndependent_vadd`, `AffineMap.affineIndependent_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`affineCombination_mem_affineSpan_pair` 📖	mathematical	`AffineIndependent` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	`AffineSubspace` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set` `Set.instInsert` `DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination` `Set.instSingletonSet` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup`	—	`vsub_vadd` `AffineSubspace.vadd_mem_iff_mem_direction` `left_mem_affineSpan_pair` `direction_affineSpan` `Finset.affineCombination_vsub` `Set.pair_comm` `weightedVSub_mem_vectorSpan_pair` `Finset.sum_congr` `Finset.sum_sub_distrib` `sub_self`
`affineIndependent_def` 📖	mathematical	—	`AffineIndependent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	—
`affineIndependent_equiv` 📖	mathematical	—	`AffineIndependent` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`Equiv.self_comp_symm` `AffineIndependent.comp_embedding`
`affineIndependent_iff` 📖	mathematical	—	`AffineIndependent` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`Finset.weightedVSub_eq_linear_combination`
`affineIndependent_iff_eq_of_fintype_affineCombination_eq` 📖	mathematical	—	`AffineIndependent`	—	`affineIndependent_iff_indicator_eq_of_affineCombination_eq` `Finset.coe_univ` `Set.indicator_univ` `Finset.sum_indicator_subset` `Finset.subset_univ` `Finset.affineCombination_indicator_subset`
`affineIndependent_iff_indicator_eq_of_affineCombination_eq` 📖	mathematical	—	`AffineIndependent` `Set.indicator` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`sub_eq_zero` `Finset.sum_congr` `Finset.sum_sub_distrib` `Finset.sum_indicator_subset` `Finset.subset_union_left` `Finset.subset_union_right` `sub_self` `Finset.affineCombination_vsub` `vsub_eq_zero_iff_eq` `Finset.affineCombination_indicator_subset` `Set.indicator_of_notMem` `Finset.sum_update_of_mem` `Finset.sum_const_zero` `add_zero` `Finset.affineCombination_of_eq_one_of_eq_zero` `Function.update_self` `Function.update_of_ne` `Finset.sum_add_distrib` `zero_add` `zero_vadd` `Set.indicator_of_mem` `Finset.mem_coe` `add_sub_cancel_right`
`affineIndependent_iff_linearIndependent_vsub` 📖	mathematical	—	`AffineIndependent` `LinearIndependent` `VSub.vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`linearIndependent_iff'` `Finset.sum_insert` `Finset.notMem_map_subtype_of_not_property` `Finset.sum_subtype_map_embedding` `neg_add_cancel` `Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero` `Finset.weightedVSubOfPoint_insert` `Finset.weightedVSubOfPoint_apply` `Finset.mem_insert_of_mem` `Finset.mem_map` `Finset.weightedVSubOfPoint_erase` `Finset.sum_subtype_of_mem` `Finset.ne_of_mem_erase` `Finset.mem_erase_of_ne_of_mem` `Finset.eq_zero_of_sum_eq_zero`
`affineIndependent_iff_of_fintype` 📖	mathematical	—	`AffineIndependent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`Finset.mem_univ` `Finset.sum_indicator_subset` `Finset.subset_univ` `Finset.weightedVSub_indicator_subset` `Set.indicator_of_mem`
`affineIndependent_of_ne` 📖	mathematical	—	`AffineIndependent` `DivisionRing.toRing` `Matrix.vecCons` `Matrix.vecEmpty`	—	`affineIndependent_iff_linearIndependent_vsub` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `Fintype.complete` `LinearIndependent.of_subsingleton` `DivisionRing.isDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Unique.instSubsingleton`
`affineIndependent_of_ne_of_mem_of_mem_of_notMem` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `SetLike.instMembership` `AffineSubspace.instSetLike`	`AffineIndependent` `Matrix.vecCons` `Matrix.vecEmpty`	—	`affineIndependent_equiv` `Fintype.complete` `affineIndependent_of_ne` `AffineIndependent.affineIndependent_of_notMem_span` `AffineSubspace.le_def'` `instIsEmptyFalse`
`affineIndependent_of_ne_of_mem_of_notMem_of_mem` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `SetLike.instMembership` `AffineSubspace.instSetLike`	`AffineIndependent` `Matrix.vecCons` `Matrix.vecEmpty`	—	`affineIndependent_equiv` `Fintype.complete` `affineIndependent_of_ne_of_mem_of_mem_of_notMem`
`affineIndependent_of_ne_of_notMem_of_mem_of_mem` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `SetLike.instMembership` `AffineSubspace.instSetLike`	`AffineIndependent` `Matrix.vecCons` `Matrix.vecEmpty`	—	`affineIndependent_equiv` `Fintype.complete` `affineIndependent_of_ne_of_mem_of_mem_of_notMem`
`affineIndependent_of_subsingleton` 📖	mathematical	—	`AffineIndependent`	—	`Fintype.eq_of_subsingleton_of_sum_eq`
`affineIndependent_set_iff_linearIndependent_vsub` 📖	mathematical	`Set` `Set.instMembership`	`AffineIndependent` `Set.Elem` `LinearIndependent` `Set.image` `VSub.vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup` `Set.instSDiff` `Set.instSingletonSet` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`affineIndependent_iff_linearIndependent_vsub` `Function.Injective.mem_set_image` `vsub_left_injective` `vadd_vsub` `Set.mem_of_mem_diff` `Set.notMem_of_mem_diff` `LinearIndependent.comp` `vadd_right_cancel` `vsub_left_cancel`
`affineIndependent_smul` 📖	mathematical	—	`AffineIndependent` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Finset.weightedVSub_eq_linear_combination` `Finset.sum_congr` `SMulCommClass.smul_comm`
`affineIndependent_vadd` 📖	mathematical	—	`AffineIndependent` `HVAdd.hVAdd` `instHVAdd` `Function.hasVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	`Finset.weightedVSub_vadd`
`exists_affineIndependent` 📖	mathematical	—	`Set` `Set.instHasSubset` `affineSpan` `DivisionRing.toRing` `AffineIndependent` `Set.instMembership`	—	`Set.eq_empty_or_nonempty` `Set.empty_subset` `affineIndependent_of_subsingleton` `IsEmpty.instSubsingleton` `Set.instIsEmptyElemEmptyCollection` `exists_linearIndependent` `LinearIndependent.ne_zero` `DivisionRing.toNontrivial` `Set.union_subset` `Set.singleton_subset_iff` `Equiv.subset_symm_image` `AffineSubspace.ext_of_direction_eq` `Submodule.span_insert_zero` `Set.image_congr` `direction_affineSpan` `vectorSpan_eq_span_vsub_set_right` `Set.mem_insert` `Equiv.coe_vaddConst_symm` `Set.image_insert_eq` `Set.image_comp` `vsub_self` `vadd_vsub` `Set.image_id'` `mem_affineSpan` `linearIndependent_set_iff_affineIndependent_vadd_union_singleton`
`exists_nontrivial_relation_sum_zero_of_not_affine_ind` 📖	mathematical	`AffineIndependent` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `Finset` `SetLike.instMembership` `Finset.instSetLike`	`Finset.sum` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Finset.instMembership`	—	`affineIndependent_iff_of_fintype` `Finset.sum_congr` `Finset.sum_dite_of_true` `Finset.mk_coe` `Finset.weightedVSub_eq_weightedVSubOfPoint_of_sum_eq_zero` `Finset.weightedVSubOfPoint_apply` `sub_zero` `zero_smul` `Subtype.coe_eta`
`exists_subset_affineIndependent_affineSpan_eq_top` 📖	mathematical	`AffineIndependent` `DivisionRing.toRing` `Set.Elem` `Set` `Set.instMembership`	`Set.instHasSubset` `affineSpan` `Top.top` `AffineSubspace` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `AffineSubspace.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`Set.eq_empty_or_nonempty` `AddTorsor.nonempty` `Module.Basis.linearIndependent` `Module.Basis.span_eq` `Module.Basis.coe_ofVectorSpace` `Module.Basis.ne_zero` `DivisionRing.toNontrivial` `Set.empty_subset` `linearIndependent_set_iff_affineIndependent_vadd_union_singleton` `affineSpan_singleton_union_vadd_eq_top_of_span_eq_top` `affineIndependent_set_iff_linearIndependent_vsub` `Set.subset_univ` `linearIndependent_subtype_iff` `LinearIndepOn.subset_extend` `Module.Basis.coe_extend` `Set.Subset.trans` `Set.image_image` `Set.image_congr` `vsub_vadd` `Set.image_id'` `Set.union_diff_self` `Set.union_subset_union_right` `Set.image_mono`
`linearIndependent_set_iff_affineIndependent_vadd_union_singleton` 📖	mathematical	—	`LinearIndependent` `Set.Elem` `Set` `Set.instMembership` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `AffineIndependent` `Set.instUnion` `Set.instSingletonSet` `Set.image` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	`affineIndependent_set_iff_linearIndependent_vsub` `Set.mem_union_left` `Set.mem_singleton` `Set.union_diff_left` `Set.image_diff` `vsub_left_injective` `Set.image_image` `Set.image_singleton` `vsub_self` `Set.image_congr` `vadd_vsub` `Set.image_id'` `Set.diff_singleton_eq_self`
`sign_eq_of_affineCombination_mem_affineSpan_pair` 📖	—	`AffineIndependent` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `AffineSubspace` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set` `Set.instInsert` `DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination` `Set.instSingletonSet` `Finset` `Finset.instMembership` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `OrderHom` `SignType` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `LinearOrder.toDecidableLT`	—	—	`affineCombination_mem_affineSpan_pair` `add_zero` `sub_zero` `sign_mul`
`sign_eq_of_affineCombination_mem_affineSpan_single_lineMap` 📖	mathematical	`AffineIndependent` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Finset` `Finset.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AffineSubspace` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set` `Set.instInsert` `Set.instSingletonSet` `DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `AffineMap.instFunLike` `AffineMap.lineMap` `Pi.addCommGroup` `Pi.Function.module` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Finset.instAddTorsorForall` `Finset.affineCombination`	`OrderHom` `SignType` `SignType.instLinearOrder` `OrderHom.instFunLike` `SignType.sign` `LinearOrder.toDecidableLT`	—	`sign_eq_of_affineCombination_mem_affineSpan_pair` `Finset.sum_affineCombinationSingleWeights` `Finset.sum_affineCombinationLineMapWeights` `Finset.affineCombination_affineCombinationLineMapWeights` `Finset.affineCombination_affineCombinationSingleWeights` `Finset.affineCombinationSingleWeights_apply_of_ne` `Finset.affineCombinationLineMapWeights_apply_left` `Finset.affineCombinationLineMapWeights_apply_right` `sign_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing`
`weightedVSub_mem_vectorSpan_pair` 📖	mathematical	`AffineIndependent` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `Set` `Set.instInsert` `DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination` `Set.instSingletonSet` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `LinearMap.instFunLike` `Finset.weightedVSub` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup`	—	`mem_vectorSpan_pair` `Finset.sum_congr` `smul_sub` `Finset.sum_sub_distrib` `sub_self` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `sub_eq_zero` `Finset.weightedVSub_const_smul` `Finset.affineCombination_vsub` `smul_eq_mul` `Finset.weightedVSub_congr`

---

← Back to Index