Basis

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

Statistics

Metric	Count
Definitions `AffineBasis`, `basisOf`, `coord`, `coords`, `instAddAction`, `instFunLike`, `instInhabitedPUnit`, `instMulAction`, `instSMul`, `instVAdd`, `reindex`, `toFun`, `finsuppAffineCoords`, `fintypeAffineCoords`	14
Theorems `affineCombination_coord_eq_self`, `basisOf_apply`, `basisOf_reindex`, `basisOf_smul`, `basisOf_vadd`, `coe_coord_of_subsingleton_eq_one`, `coe_reindex`, `coe_smul`, `coe_vadd`, `coord_apply`, `coord_apply_centroid`, `coord_apply_combination_of_mem`, `coord_apply_combination_of_notMem`, `coord_apply_eq`, `coord_apply_ne`, `coord_reindex`, `coord_smul`, `coord_vadd`, `coords_apply`, `exists_affineBasis`, `exists_affine_subbasis`, `ext`, `ext_elem`, `ext_iff`, `ind`, `ind'`, `instIsScalarTower`, `instSMulCommClass`, `linear_combination_coord_eq_self`, `linear_eq_sumCoords`, `nonempty`, `reindex_apply`, `reindex_refl`, `reindex_smul`, `sum_coord_apply_eq_one`, `surjective_coord`, `tot`, `tot'`, `injOn_affineCombination_fintypeAffineCoords`, `mem_finsuppAffineCoords_iff_linearCombination`, `mem_fintypeAffineCoords_iff_sum`	41
Total	55

AffineBasis

Definitions

Name	Category	Theorems
`basisOf` 📖	CompOp	5 math math: `linear_eq_sumCoords`, `basisOf_smul`, `basisOf_reindex`, `basisOf_vadd`, `basisOf_apply`
`coord` 📖	CompOp	20 math math: `smooth_barycentric_coord`, `linear_eq_sumCoords`, `coord_apply_ne`, `coord_apply`, `coord_reindex`, `toMatrix_apply`, `sum_coord_apply_eq_one`, `coord_apply_combination_of_notMem`, `coord_apply_eq`, `coord_apply_centroid`, `continuous_barycentric_coord`, `coords_apply`, `surjective_coord`, `coord_vadd`, `isOpenMap_barycentric_coord`, `affineCombination_coord_eq_self`, `coe_coord_of_subsingleton_eq_one`, `coord_smul`, `coord_apply_combination_of_mem`, `linear_combination_coord_eq_self`
`coords` 📖	CompOp	4 math math: `toMatrix_vecMul_coords`, `det_smul_coords_eq_cramer_coords`, `toMatrix_inv_vecMul_toMatrix`, `coords_apply`
`instAddAction` 📖	CompOp	—
`instFunLike` 📖	CompOp	28 math math: `tot`, `coe_smul`, `coord_apply_ne`, `convexHull_eq_nonneg_coord`, `coord_apply`, `toMatrix_mul_toMatrix`, `coe_vadd`, `interior_convexHull`, `coe_reindex`, `ind`, `exists_mem_interior_convexHull_affineBasis`, `toMatrix_vecMul_coords`, `det_smul_coords_eq_cramer_coords`, `coord_apply_combination_of_notMem`, `exists_affineBasis`, `coord_apply_eq`, `coord_apply_centroid`, `ext_iff`, `toMatrix_inv_vecMul_toMatrix`, `reindex_apply`, `centroid_mem_interior_convexHull`, `affineCombination_coord_eq_self`, `toMatrix_self`, `exists_affine_subbasis`, `coord_apply_combination_of_mem`, `linear_combination_coord_eq_self`, `isUnit_toMatrix`, `basisOf_apply`
`instInhabitedPUnit` 📖	CompOp	—
`instMulAction` 📖	CompOp	—
`instSMul` 📖	CompOp	6 math math: `coe_smul`, `basisOf_smul`, `reindex_smul`, `instIsScalarTower`, `instSMulCommClass`, `coord_smul`
`instVAdd` 📖	CompOp	3 math math: `coe_vadd`, `coord_vadd`, `basisOf_vadd`
`reindex` 📖	CompOp	6 math math: `coord_reindex`, `reindex_refl`, `reindex_smul`, `coe_reindex`, `basisOf_reindex`, `reindex_apply`
`toFun` 📖	CompOp	2 math math: `tot'`, `ind'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`affineCombination_coord_eq_self` 📖	mathematical	—	`DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination` `Finset.univ` `AffineBasis` `instFunLike` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `coord`	—	`tot` `AffineSubspace.mem_top` `eq_affineCombination_of_mem_affineSpan_of_fintype` `coord_apply_combination_of_mem` `Finset.mem_univ`
`basisOf_apply` 📖	mathematical	—	`DFunLike.coe` `Module.Basis` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Module.Basis.instFunLike` `basisOf` `VSub.vsub` `AddTorsor.toVSub` `AddCommGroup.toAddGroup` `AffineBasis` `instFunLike`	—	—
`basisOf_reindex` 📖	mathematical	—	`basisOf` `reindex` `Module.Basis.reindex` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Equiv.subtypeEquiv` `Iff.not` `Equiv.eq_symm_apply`	—	`Module.Basis.eq_of_apply_eq` `Iff.not` `Equiv.eq_symm_apply` `basisOf_apply` `Module.Basis.coe_reindex`
`basisOf_smul` 📖	mathematical	—	`basisOf` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `AffineBasis` `instSMul` `Module.Basis` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Module.Basis.instSMul`	—	`Module.Basis.eq_of_apply_eq` `basisOf_apply` `smul_sub`
`basisOf_vadd` 📖	mathematical	—	`basisOf` `HVAdd.hVAdd` `AffineBasis` `instHVAdd` `instVAdd`	—	`Module.Basis.eq_of_apply_eq` `basisOf_apply` `vadd_vsub_vadd_cancel_left`
`coe_coord_of_subsingleton_eq_one` 📖	mathematical	—	`DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `coord` `Pi.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`Set.image_univ` `Set.Subsingleton.image` `Set.subsingleton_of_subsingleton` `Finset.sum_congr` `Finset.sum_const` `Finset.card_singleton` `one_smul` `AffineSubspace.subsingleton_of_subsingleton_span_eq_top` `tot` `Pi.one_apply` `coord_apply_combination_of_mem`
`coe_reindex` 📖	mathematical	—	`DFunLike.coe` `AffineBasis` `instFunLike` `reindex` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	—
`coe_smul` 📖	mathematical	—	`DFunLike.coe` `AffineBasis` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instFunLike` `instSMul` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`coe_vadd` 📖	mathematical	—	`DFunLike.coe` `AffineBasis` `instFunLike` `HVAdd.hVAdd` `instHVAdd` `instVAdd` `Function.hasVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	—
`coord_apply` 📖	mathematical	—	`DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `coord` `AffineBasis` `instFunLike` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`eq_or_ne` `coord_apply_eq` `coord_apply_ne`
`coord_apply_centroid` 📖	mathematical	`Finset` `Finset.instMembership`	`DFunLike.coe` `AffineMap` `DivisionRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `coord` `Finset.centroid` `AffineBasis` `instFunLike` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Finset.card`	—	`Finset.centroid.eq_1` `coord_apply_combination_of_mem` `Finset.sum_centroidWeights_eq_one_of_nonempty` `Finset.centroidWeights.eq_1`
`coord_apply_combination_of_mem` 📖	mathematical	`Finset` `Finset.instMembership` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	`DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `AffineMap.instFunLike` `coord` `Pi.addCommGroup` `Pi.Function.module` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Finset.instAddTorsorForall` `Finset.affineCombination` `AffineBasis` `instFunLike`	—	`Finset.map_affineCombination` `Finset.affineCombination_eq_linear_combination` `Finset.sum_congr` `coord_apply` `mul_boole` `Finset.sum_ite_eq`
`coord_apply_combination_of_notMem` 📖	mathematical	`Finset` `Finset.instMembership` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	`DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `AffineMap.instFunLike` `coord` `Pi.addCommGroup` `Pi.Function.module` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Finset.instAddTorsorForall` `Finset.affineCombination` `AffineBasis` `instFunLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Finset.map_affineCombination` `Finset.affineCombination_eq_linear_combination` `Finset.sum_congr` `coord_apply` `mul_boole` `Finset.sum_ite_eq`
`coord_apply_eq` 📖	mathematical	—	`DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `coord` `AffineBasis` `instFunLike` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`RingHomInvPair.ids` `vsub_self` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `sub_zero`
`coord_apply_ne` 📖	mathematical	—	`DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `coord` `AffineBasis` `instFunLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`coord.eq_1` `basisOf_apply` `Module.Basis.sumCoords_self_apply` `sub_self`
`coord_reindex` 📖	mathematical	—	`coord` `reindex` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	`AffineMap.ext` `RingHomInvPair.ids` `Iff.not` `Equiv.eq_symm_apply` `basisOf_reindex` `Module.Basis.sumCoords_reindex`
`coord_smul` 📖	mathematical	—	`coord` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `AffineBasis` `instSMul` `AffineMap.comp` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `LinearMap.toAffineMap` `LinearEquiv.toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `LinearEquiv.symm` `DistribMulAction.toLinearEquiv`	—	`AffineMap.ext` `RingHomInvPair.ids` `basisOf_smul` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `inv_smul_smul`
`coord_vadd` 📖	mathematical	—	`coord` `HVAdd.hVAdd` `AffineBasis` `instHVAdd` `instVAdd` `AffineMap.comp` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineEquiv.toAffineMap` `AffineEquiv.symm` `AffineEquiv.constVAdd`	—	`AffineMap.ext` `RingHomInvPair.ids` `basisOf_vadd` `AffineEquiv.constVAdd_symm` `vadd_vsub_assoc` `neg_add_eq_sub` `vsub_vadd_eq_vsub_sub`
`coords_apply` 📖	mathematical	—	`DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `coords` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `coord`	—	—
`exists_affineBasis` 📖	mathematical	—	`DFunLike.coe` `AffineBasis` `Set.Elem` `DivisionRing.toRing` `instFunLike` `Set` `Set.instMembership`	—	`exists_affine_subbasis` `AffineSubspace.span_univ`
`exists_affine_subbasis` 📖	mathematical	`affineSpan` `DivisionRing.toRing` `Top.top` `AffineSubspace` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `AffineSubspace.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`Set` `Set.instHasSubset` `DFunLike.coe` `AffineBasis` `Set.Elem` `instFunLike` `Set.instMembership`	—	`exists_affineIndependent` `Subtype.range_coe`
`ext` 📖	—	`DFunLike.coe` `AffineBasis` `instFunLike`	—	—	`DFunLike.coe_injective`
`ext_elem` 📖	—	`DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `coord`	—	—	`nonempty_fintype` `affineCombination_coord_eq_self`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `AffineBasis` `instFunLike`	—	`ext`
`ind` 📖	mathematical	—	`AffineIndependent` `DFunLike.coe` `AffineBasis` `instFunLike`	—	`ind'`
`ind'` 📖	mathematical	—	`AffineIndependent` `toFun`	—	—
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `AffineBasis` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instSMul`	—	`DFunLike.ext` `smul_assoc`
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `AffineBasis` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `instSMul`	—	`DFunLike.ext` `SMulCommClass.smul_comm`
`linear_combination_coord_eq_self` 📖	mathematical	—	`Finset.sum` `AddCommGroup.toAddCommMonoid` `Finset.univ` `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` `DFunLike.coe` `AffineMap` `addGroupIsAddTorsor` `Ring.toAddCommGroup` `Semiring.toModule` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `coord` `AffineBasis` `instFunLike`	—	`affineCombination_coord_eq_self` `Finset.affineCombination_eq_linear_combination` `sum_coord_apply_eq_one`
`linear_eq_sumCoords` 📖	mathematical	—	`AffineMap.linear` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `coord` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.instNeg` `Module.Basis.sumCoords` `basisOf`	—	—
`nonempty` 📖	—	—	—	—	`not_isEmpty_iff` `Set.range_eq_empty` `AffineSubspace.span_empty` `AffineSubspace.instNontrivial` `tot`
`reindex_apply` 📖	mathematical	—	`DFunLike.coe` `AffineBasis` `instFunLike` `reindex` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	—
`reindex_refl` 📖	mathematical	—	`reindex` `Equiv.refl`	—	`ext`
`reindex_smul` 📖	mathematical	—	`reindex` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `AffineBasis` `instSMul`	—	—
`sum_coord_apply_eq_one` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finset.univ` `DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `coord` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`tot` `AffineSubspace.mem_top` `eq_affineCombination_of_mem_affineSpan_of_fintype` `Finset.sum_congr` `coord_apply_combination_of_mem` `Finset.mem_univ`
`surjective_coord` 📖	mathematical	—	`DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `coord`	—	`exists_ne` `Finset.sum_congr` `Finset.sum_ite` `Finset.filter_insert` `Finset.filter_false_of_mem` `Finset.instLawfulSingleton` `Finset.sum_const` `Finset.card_singleton` `one_smul` `Finset.filter_true_of_mem` `Finset.sum_sub_distrib` `add_sub_cancel` `coord_apply_combination_of_mem`
`tot` 📖	mathematical	—	`affineSpan` `Set.range` `DFunLike.coe` `AffineBasis` `instFunLike` `Top.top` `AffineSubspace` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `AffineSubspace.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`tot'`
`tot'` 📖	mathematical	—	`affineSpan` `Set.range` `toFun` `Top.top` `AffineSubspace` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `AffineSubspace.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	—

AffineIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`injOn_affineCombination_fintypeAffineCoords` 📖	mathematical	`AffineIndependent`	`Set.InjOn` `DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination` `Finset.univ` `SetLike.coe` `AffineSubspace` `AffineSubspace.instSetLike` `fintypeAffineCoords`	—	`affineIndependent_iff_eq_of_fintype_affineCombination_eq` `mem_fintypeAffineCoords_iff_sum`

(root)

Definitions

Name	Category	Theorems
`AffineBasis` 📖	CompData	36 math math: `AffineBasis.tot`, `AffineBasis.coe_smul`, `AffineBasis.coord_apply_ne`, `AffineBasis.convexHull_eq_nonneg_coord`, `AffineBasis.coord_apply`, `AffineBasis.toMatrix_mul_toMatrix`, `AffineBasis.coe_vadd`, `AffineBasis.interior_convexHull`, `AffineBasis.basisOf_smul`, `AffineBasis.reindex_smul`, `AffineBasis.coe_reindex`, `AffineBasis.ind`, `exists_mem_interior_convexHull_affineBasis`, `AffineBasis.toMatrix_vecMul_coords`, `AffineBasis.instIsScalarTower`, `AffineBasis.det_smul_coords_eq_cramer_coords`, `AffineBasis.coord_apply_combination_of_notMem`, `AffineBasis.exists_affineBasis`, `AffineBasis.coord_apply_eq`, `AffineBasis.coord_apply_centroid`, `AffineBasis.instSMulCommClass`, `AffineBasis.ext_iff`, `AffineBasis.toMatrix_inv_vecMul_toMatrix`, `AffineBasis.coord_vadd`, `AffineBasis.reindex_apply`, `AffineBasis.centroid_mem_interior_convexHull`, `AffineBasis.affineCombination_coord_eq_self`, `AffineBasis.toMatrix_self`, `AffineBasis.exists_affine_subbasis`, `AffineBasis.coord_smul`, `AffineBasis.coord_apply_combination_of_mem`, `AffineBasis.linear_combination_coord_eq_self`, `AffineBasis.isUnit_toMatrix`, `AffineBasis.exists_affineBasis_of_finiteDimensional`, `AffineBasis.basisOf_vadd`, `AffineBasis.basisOf_apply`
`finsuppAffineCoords` 📖	CompOp	1 math math: `mem_finsuppAffineCoords_iff_linearCombination`
`fintypeAffineCoords` 📖	CompOp	2 math math: `mem_fintypeAffineCoords_iff_sum`, `AffineIndependent.injOn_affineCombination_fintypeAffineCoords`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_finsuppAffineCoords_iff_linearCombination` 📖	mathematical	—	`Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AffineSubspace` `Finsupp.instAddCommGroup` `Ring.toAddCommGroup` `Finsupp.module` `Ring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule` `addGroupIsAddTorsor` `Finsupp.instAddGroup` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `SetLike.instMembership` `AffineSubspace.instSetLike` `finsuppAffineCoords` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `LinearMap.instFunLike` `Finsupp.linearCombination` `Pi.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	—
`mem_fintypeAffineCoords_iff_sum` 📖	mathematical	—	`AffineSubspace` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `SetLike.instMembership` `AffineSubspace.instSetLike` `fintypeAffineCoords` `Finset.sum` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finset.univ` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`Finset.sum_congr` `mul_one`

---

← Back to Index