FiniteDimensional

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

Statistics

Metric	Count
Definitions `Collinear`, `Coplanar`	2
Theorems `collinear_point_centroid_faceOppositeCentroid`, `span_eq_top`, `card_eq_finrank_add_one`, `exists_affineBasis_of_finiteDimensional`, `finite`, `finiteDimensional`, `finite_set`, `affineSpan_eq_of_le_of_card_eq_finrank_add_one`, `affineSpan_eq_top_iff_card_eq_finrank_add_one`, `affineSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one`, `card_le_card_of_subset_affineSpan`, `card_le_finrank_succ`, `card_lt_card_of_affineSpan_lt_affineSpan`, `finrank_vectorSpan`, `finrank_vectorSpan_add_one`, `finrank_vectorSpan_image_finset`, `vectorSpan_eq_of_le_of_card_eq_finrank_add_one`, `vectorSpan_eq_top_of_card_eq_finrank_add_one`, `vectorSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one`, `finiteDimensional_sup`, `affineSpan_eq_of_ne`, `collinear_insert_iff_of_ne`, `coplanar`, `coplanar_insert`, `finiteDimensional_direction_affineSpan`, `finiteDimensional_vectorSpan`, `finrank_le_one`, `mem_affineSpan_of_mem_of_ne`, `subset`, `finiteDimensional_direction_affineSpan`, `finiteDimensional_vectorSpan`, `finrank_le_two`, `subset`, `affineIndependent_iff_affineIndependent_collinear_ne`, `affineIndependent_iff_finrank_vectorSpan_eq`, `affineIndependent_iff_le_finrank_vectorSpan`, `affineIndependent_iff_not_collinear`, `affineIndependent_iff_not_collinear_of_ne`, `affineIndependent_iff_not_collinear_set`, `affineIndependent_iff_not_finrank_vectorSpan_le`, `affineIndependent_of_affineIndependent_collinear_ne`, `collinear_empty`, `collinear_iff_exists_forall_eq_smul_vadd`, `collinear_iff_finrank_le_one`, `collinear_iff_not_affineIndependent`, `collinear_iff_not_affineIndependent_of_ne`, `collinear_iff_not_affineIndependent_set`, `collinear_iff_of_mem`, `collinear_iff_rank_le_one`, `collinear_insert_iff_of_mem_affineSpan`, `collinear_insert_insert_insert_left_of_mem_affineSpan_pair`, `collinear_insert_insert_insert_of_mem_affineSpan_pair`, `collinear_insert_insert_of_mem_affineSpan_pair`, `collinear_insert_of_mem_affineSpan_pair`, `collinear_pair`, `collinear_singleton`, `collinear_triple_of_mem_affineSpan_pair`, `coplanar_empty`, `coplanar_iff_finrank_le_two`, `coplanar_insert_iff_of_mem_affineSpan`, `coplanar_of_fact_finrank_eq_two`, `coplanar_of_finrank_eq_two`, `coplanar_pair`, `coplanar_singleton`, `coplanar_triple`, `finiteDimensional_direction_affineSpan_image_of_finite`, `finiteDimensional_direction_affineSpan_insert`, `finiteDimensional_direction_affineSpan_insert_set`, `finiteDimensional_direction_affineSpan_of_finite`, `finiteDimensional_direction_affineSpan_range`, `finiteDimensional_direction_affineSpan_singleton`, `finiteDimensional_direction_map`, `finiteDimensional_vectorSpan_image_of_finite`, `finiteDimensional_vectorSpan_insert`, `finiteDimensional_vectorSpan_insert_set`, `finiteDimensional_vectorSpan_of_finite`, `finiteDimensional_vectorSpan_range`, `finiteDimensional_vectorSpan_singleton`, `finite_of_fin_dim_affineIndependent`, `finite_set_of_fin_dim_affineIndependent`, `finrank_vectorSpan_image_finset_le`, `finrank_vectorSpan_insert_le`, `finrank_vectorSpan_insert_le_set`, `finrank_vectorSpan_le_iff_not_affineIndependent`, `finrank_vectorSpan_range_add_one_le`, `finrank_vectorSpan_range_le`, `ne₁₂_of_not_collinear`, `ne₁₃_of_not_collinear`, `ne₂₃_of_not_collinear`	89
Total	91

Affine.Simplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`collinear_point_centroid_faceOppositeCentroid` 📖	mathematical	—	`Collinear` `Set` `Set.instInsert` `points` `DivisionRing.toRing` `centroid` `Set.instSingletonSet` `faceOppositeCentroid`	—	`collinear_insert_of_mem_affineSpan_pair` `neg_vsub_eq_vsub_rev` `neg_smul_neg` `point_vsub_centroid_eq_smul_vsub` `vsub_vadd` `smul_vsub_vadd_mem_affineSpan_pair`
`span_eq_top` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	`affineSpan` `DivisionRing.toRing` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `Set.range` `points` `Top.top` `AffineSubspace` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `AffineSubspace.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_one` `independent` `Fintype.card_fin`

AffineBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_eq_finrank_add_one` 📖	mathematical	—	`Fintype.card` `Module.finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	—	`finiteDimensional` `Finite.of_fintype` `AffineIndependent.affineSpan_eq_top_iff_card_eq_finrank_add_one` `ind` `tot`
`exists_affineBasis_of_finiteDimensional` 📖	mathematical	`Fintype.card` `Module.finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	`AffineBasis` `DivisionRing.toRing`	—	`exists_affineBasis` `CanLift.prf` `Set.instCanLiftFinsetCoeFinite` `finite_set` `card_eq_finrank_add_one`
`finite` 📖	mathematical	—	`Finite`	—	`finite_of_fin_dim_affineIndependent` `ind`
`finiteDimensional` 📖	mathematical	—	`FiniteDimensional`	—	`nonempty` `Module.Basis.finiteDimensional_of_finite` `Subtype.finite`
`finite_set` 📖	mathematical	—	`Set.Finite`	—	`finite_set_of_fin_dim_affineIndependent` `ind`

AffineIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`affineSpan_eq_of_le_of_card_eq_finrank_add_one` 📖	—	`AffineIndependent` `DivisionRing.toRing` `AffineSubspace` `Preorder.toLE` `PartialOrder.toPreorder` `AffineSubspace.instPartialOrder` `affineSpan` `Set.range` `Fintype.card` `Module.finrank` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `AffineSubspace.direction` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module`	—	—	`Set.image_univ` `Finset.coe_univ` `Finset.coe_image` `affineSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one` `Finset.card_univ`
`affineSpan_eq_top_iff_card_eq_finrank_add_one` 📖	mathematical	`AffineIndependent` `DivisionRing.toRing`	`affineSpan` `Set.range` `Top.top` `AffineSubspace` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `AffineSubspace.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Fintype.card` `Module.finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	—	`AffineSubspace.card_pos_of_affineSpan_eq_top` `finrank_top` `AffineSubspace.vectorSpan_eq_top_of_affineSpan_eq_top` `finrank_vectorSpan` `affineSpan_eq_of_le_of_card_eq_finrank_add_one` `FiniteDimensional.finiteDimensional_submodule` `le_top` `AffineSubspace.direction_top`
`affineSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one` 📖	—	`AffineIndependent` `DivisionRing.toRing` `AffineSubspace` `Preorder.toLE` `PartialOrder.toPreorder` `AffineSubspace.instPartialOrder` `affineSpan` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.image` `Finset.card` `Module.finrank` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `AffineSubspace.direction` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module`	—	—	`Finset.card_pos` `AffineSubspace.eq_of_direction_eq_of_nonempty_of_le` `AffineSubspace.direction_le` `direction_affineSpan` `vectorSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one` `Set.Nonempty.affineSpan` `Finset.Nonempty.to_set` `Finset.Nonempty.image`
`card_le_card_of_subset_affineSpan` 📖	mathematical	`AffineIndependent` `DivisionRing.toRing` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Set` `Set.instHasSubset` `SetLike.coe` `AffineSubspace` `AffineSubspace.instSetLike` `affineSpan`	`Finset.card`	—	`Finset.eq_empty_or_nonempty` `Nat.instCanonicallyOrderedAdd` `Finset.coe_empty` `AffineSubspace.span_empty` `Finset.Nonempty.to_subtype` `Set.Nonempty.to_subtype` `Finset.Nonempty.to_set` `AffineSubspace.direction_le` `affineSpan_mono` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Submodule.finrank_mono` `IsNoetherianRing.strongRankCondition` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing` `finiteDimensional_vectorSpan_range` `Finite.of_fintype` `Subtype.range_coe` `direction_affineSpan` `AffineSubspace.affineSpan_coe` `Fintype.card_coe` `Fintype.card_congr'` `LE.le.trans` `finrank_vectorSpan_add_one` `finrank_vectorSpan_range_add_one_le`
`card_le_finrank_succ` 📖	mathematical	`AffineIndependent` `DivisionRing.toRing`	`Fintype.card` `Module.finrank` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `Set.range` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module`	—	`isEmpty_or_nonempty` `Fintype.card_eq_zero` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `tsub_le_iff_right` `Nat.instOrderedSub` `affineIndependent_iff_le_finrank_vectorSpan` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Fintype.card_ne_zero`
`card_lt_card_of_affineSpan_lt_affineSpan` 📖	mathematical	`AffineIndependent` `DivisionRing.toRing` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `Finset` `SetLike.instMembership` `Finset.instSetLike` `AffineSubspace` `Preorder.toLT` `PartialOrder.toPreorder` `AffineSubspace.instPartialOrder` `affineSpan` `SetLike.coe`	`Finset.card`	—	`Finset.eq_empty_or_nonempty` `Finset.coe_empty` `AffineSubspace.span_empty` `Finset.Nonempty.to_subtype` `Set.Nonempty.to_subtype` `Finset.Nonempty.to_set` `AffineSubspace.direction_lt_of_nonempty` `Set.Nonempty.affineSpan` `add_lt_add_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Submodule.finrank_lt_finrank_of_lt` `finiteDimensional_vectorSpan_range` `Finite.of_fintype` `Subtype.range_coe` `direction_affineSpan` `Fintype.card_coe` `Fintype.card_congr'` `LT.lt.trans_le` `finrank_vectorSpan_add_one` `finrank_vectorSpan_range_add_one_le`
`finrank_vectorSpan` 📖	mathematical	`AffineIndependent` `DivisionRing.toRing` `Fintype.card`	`Module.finrank` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `Set.range` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module`	—	`Set.image_univ` `Finset.coe_univ` `Finset.coe_image` `finrank_vectorSpan_image_finset` `Finset.card_univ`
`finrank_vectorSpan_add_one` 📖	mathematical	`AffineIndependent` `DivisionRing.toRing`	`Module.finrank` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `Set.range` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module` `Fintype.card`	—	`finrank_vectorSpan` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `Fintype.card_pos`
`finrank_vectorSpan_image_finset` 📖	mathematical	`AffineIndependent` `DivisionRing.toRing` `Finset.card`	`Module.finrank` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.image` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module`	—	`mono` `range` `Set.image_subset_range` `Finset.card_image_of_injective` `injective` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instNoMaxOrder` `Nat.instCanonicallyOrderedAdd` `vsub_left_injective` `Finset.card_erase_of_mem` `vectorSpan_eq_span_vsub_finset_right_ne` `finrank_span_finset_eq_card` `IsNoetherianRing.strongRankCondition` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing` `Finset.coe_image` `Finset.sdiff_singleton_eq_erase` `Finset.coe_sdiff` `Finset.coe_singleton` `affineIndependent_set_iff_linearIndependent_vsub`
`vectorSpan_eq_of_le_of_card_eq_finrank_add_one` 📖	—	`AffineIndependent` `DivisionRing.toRing` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `vectorSpan` `Set.range` `Fintype.card` `Module.finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	—	—	`Submodule.eq_of_le_of_finrank_eq` `finrank_vectorSpan`
`vectorSpan_eq_top_of_card_eq_finrank_add_one` 📖	mathematical	`AffineIndependent` `DivisionRing.toRing` `Fintype.card` `Module.finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	`vectorSpan` `Set.range` `Top.top` `Submodule` `Ring.toSemiring` `Submodule.instTop`	—	`Submodule.eq_top_of_finrank_eq` `finrank_vectorSpan`
`vectorSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one` 📖	—	`AffineIndependent` `DivisionRing.toRing` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `vectorSpan` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.image` `Finset.card` `Module.finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	—	—	`Submodule.eq_of_le_of_finrank_eq` `finrank_vectorSpan_image_finset`

AffineSubspace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finiteDimensional_sup` 📖	mathematical	—	`FiniteDimensional` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `direction` `AffineSubspace` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Submodule.addCommGroup` `Submodule.module`	—	`eq_bot_or_nonempty` `bot_sup_eq` `sup_bot_eq` `direction_sup` `Submodule.finiteDimensional_sup` `FiniteDimensional.span_singleton`

Collinear

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`affineSpan_eq_of_ne` 📖	mathematical	`Collinear` `Set` `Set.instMembership`	`affineSpan` `DivisionRing.toRing` `Set.instInsert` `Set.instSingletonSet`	—	`le_antisymm` `affineSpan_mono` `Set.insert_subset_iff` `Set.singleton_subset_iff` `affineSpan_le` `mem_affineSpan_of_mem_of_ne`
`collinear_insert_iff_of_ne` 📖	mathematical	`Collinear` `Set` `Set.instMembership`	`Set.instInsert` `Set.instSingletonSet`	—	`direction_affineSpan` `affineSpan_insert_affineSpan` `affineSpan_eq_of_ne` `eq_1`
`coplanar` 📖	mathematical	`Collinear`	`Coplanar`	—	`le_trans` `one_le_two` `IsOrderedRing.toZeroLEOneClass` `Cardinal.isOrderedRing` `Cardinal.addLeftMono`
`coplanar_insert` 📖	mathematical	`Collinear`	`Coplanar` `Set` `Set.instInsert`	—	`finiteDimensional_vectorSpan` `coplanar_iff_finrank_le_two` `finiteDimensional_vectorSpan_insert_set` `le_imp_le_of_le_of_le` `finrank_vectorSpan_insert_le_set` `le_refl` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `finrank_le_one`
`finiteDimensional_direction_affineSpan` 📖	mathematical	`Collinear`	`FiniteDimensional` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `AffineSubspace.direction` `affineSpan` `Submodule.addCommGroup` `Submodule.module`	—	`finiteDimensional_vectorSpan` `direction_affineSpan`
`finiteDimensional_vectorSpan` 📖	mathematical	`Collinear`	`FiniteDimensional` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `Submodule.addCommGroup` `Submodule.module`	—	`IsNoetherian.iff_fg` `IsNoetherian.iff_rank_lt_aleph0` `lt_of_le_of_lt` `Cardinal.one_lt_aleph0`
`finrank_le_one` 📖	mathematical	`Collinear`	`Module.finrank` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module`	—	`collinear_iff_finrank_le_one`
`mem_affineSpan_of_mem_of_ne` 📖	mathematical	`Collinear` `Set` `Set.instMembership`	`AffineSubspace` `DivisionRing.toRing` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set.instInsert` `Set.instSingletonSet`	—	`collinear_iff_of_mem` `vadd_left_mem_affineSpan_pair` `zero_smul` `zero_vadd` `vadd_vsub` `smul_smul` `IsUnit.div_mul_cancel`
`subset` 📖	—	`Set` `Set.instHasSubset` `Collinear`	—	—	`LE.le.trans` `Submodule.rank_mono` `vectorSpan_mono`

Coplanar

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finiteDimensional_direction_affineSpan` 📖	mathematical	`Coplanar`	`FiniteDimensional` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `AffineSubspace.direction` `affineSpan` `Submodule.addCommGroup` `Submodule.module`	—	`finiteDimensional_vectorSpan` `direction_affineSpan`
`finiteDimensional_vectorSpan` 📖	mathematical	`Coplanar`	`FiniteDimensional` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `Submodule.addCommGroup` `Submodule.module`	—	`IsNoetherian.iff_fg` `IsNoetherian.iff_rank_lt_aleph0` `lt_of_le_of_lt` `Cardinal.lt_aleph0`
`finrank_le_two` 📖	mathematical	`Coplanar`	`Module.finrank` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module`	—	`coplanar_iff_finrank_le_two`
`subset` 📖	—	`Set` `Set.instHasSubset` `Coplanar`	—	—	`LE.le.trans` `Submodule.rank_mono` `vectorSpan_mono`

(root)

Definitions

Name	Category	Theorems
`Collinear` 📖	MathDef	33 math math: `collinear_singleton`, `affineIndependent_iff_not_collinear_set`, `EuclideanGeometry.oangle_sign_eq_zero_iff_collinear`, `collinear_insert_insert_insert_left_of_mem_affineSpan_pair`, `EuclideanGeometry.collinear_iff_of_two_zsmul_oangle_eq`, `Wbtw.collinear`, `collinear_iff_of_mem`, `EuclideanGeometry.Sphere.secondInter_collinear`, `collinear_pair`, `collinear_iff_not_affineIndependent_of_ne`, `collinear_insert_insert_insert_of_mem_affineSpan_pair`, `EuclideanGeometry.collinear_of_angle_eq_zero`, `collinear_iff_finrank_le_one`, `EuclideanGeometry.oangle_eq_zero_or_eq_pi_iff_collinear`, `EuclideanGeometry.collinear_iff_eq_or_eq_or_sin_eq_zero`, `EuclideanGeometry.cospherical_or_collinear_of_two_zsmul_oangle_eq`, `affineIndependent_iff_not_collinear_of_ne`, `collinear_iff_rank_le_one`, `collinear_insert_insert_of_mem_affineSpan_pair`, `collinear_triple_of_mem_affineSpan_pair`, `EuclideanGeometry.collinear_of_sin_eq_zero`, `Affine.Simplex.collinear_point_centroid_faceOppositeCentroid`, `EuclideanGeometry.collinear_of_angle_eq_pi`, `EuclideanGeometry.oangle_ne_zero_and_ne_pi_iff_not_collinear`, `EuclideanGeometry.collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi`, `collinear_insert_of_mem_affineSpan_pair`, `affineIndependent_iff_not_collinear`, `collinear_iff_not_affineIndependent_set`, `collinear_insert_iff_of_mem_affineSpan`, `collinear_iff_exists_forall_eq_smul_vadd`, `EuclideanGeometry.concyclic_or_collinear_of_two_zsmul_oangle_eq`, `collinear_iff_not_affineIndependent`, `collinear_empty`
`Coplanar` 📖	MathDef	11 math math: `coplanar_empty`, `coplanar_of_fact_finrank_eq_two`, `Collinear.coplanar_insert`, `EuclideanGeometry.Concyclic.Coplanar`, `coplanar_pair`, `coplanar_of_finrank_eq_two`, `Collinear.coplanar`, `coplanar_triple`, `coplanar_iff_finrank_le_two`, `coplanar_insert_iff_of_mem_affineSpan`, `coplanar_singleton`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`affineIndependent_iff_affineIndependent_collinear_ne` 📖	mathematical	`Collinear` `Set` `Set.instInsert` `Set.instSingletonSet`	`AffineIndependent` `DivisionRing.toRing` `Matrix.vecCons` `Matrix.vecEmpty`	—	`affineIndependent_of_affineIndependent_collinear_ne` `Set.ext`
`affineIndependent_iff_finrank_vectorSpan_eq` 📖	mathematical	`Fintype.card`	`AffineIndependent` `DivisionRing.toRing` `Module.finrank` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `Set.range` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module`	—	`IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.instNoMaxOrder` `Nat.instCanonicallyOrderedAdd` `affineIndependent_iff_linearIndependent_vsub` `linearIndependent_iff_card_eq_finrank_span` `IsNoetherianRing.orzechProperty` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `vectorSpan_range_eq_span_range_vsub_right_ne` `Set.finrank.eq_1` `Fintype.subtype_card` `Finset.filter_ne'` `Finset.card_erase_of_mem` `Finset.card_univ` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`affineIndependent_iff_le_finrank_vectorSpan` 📖	mathematical	`Fintype.card`	`AffineIndependent` `DivisionRing.toRing` `Module.finrank` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `Set.range` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module`	—	`affineIndependent_iff_finrank_vectorSpan_eq` `le_refl` `le_antisymm` `finrank_vectorSpan_range_le`
`affineIndependent_iff_not_collinear` 📖	mathematical	—	`AffineIndependent` `DivisionRing.toRing` `Collinear` `Set.range`	—	`collinear_iff_finrank_le_one` `finiteDimensional_vectorSpan_range` `Finite.of_fintype` `affineIndependent_iff_not_finrank_vectorSpan_le` `Fintype.card_fin`
`affineIndependent_iff_not_collinear_of_ne` 📖	mathematical	—	`AffineIndependent` `DivisionRing.toRing` `Collinear` `Set` `Set.instInsert` `Set.instSingletonSet`	—	`affineIndependent_iff_not_collinear` `Set.image_univ` `Finset.coe_univ` `Finset.coe_insert` `Finset.coe_singleton` `Set.image_insert_eq` `Set.image_pair`
`affineIndependent_iff_not_collinear_set` 📖	mathematical	—	`AffineIndependent` `DivisionRing.toRing` `Matrix.vecCons` `Matrix.vecEmpty` `Collinear` `Set` `Set.instInsert` `Set.instSingletonSet`	—	`affineIndependent_iff_not_collinear` `Matrix.range_cons` `Matrix.range_empty` `Set.instLawfulSingleton`
`affineIndependent_iff_not_finrank_vectorSpan_le` 📖	mathematical	`Fintype.card`	`AffineIndependent` `DivisionRing.toRing` `Module.finrank` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `Set.range` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module`	—	`affineIndependent_iff_le_finrank_vectorSpan` `lt_iff_not_ge`
`affineIndependent_of_affineIndependent_collinear_ne` 📖	—	`AffineIndependent` `DivisionRing.toRing` `Matrix.vecCons` `Matrix.vecEmpty` `Collinear` `Set` `Set.instInsert` `Set.instSingletonSet`	—	—	`affineIndependent_iff_not_collinear_set` `collinear_insert_insert_of_mem_affineSpan_pair` `Collinear.mem_affineSpan_of_mem_of_ne` `Collinear.subset`
`collinear_empty` 📖	mathematical	—	`Collinear` `Set` `Set.instEmptyCollection`	—	`collinear_iff_rank_le_one` `vectorSpan_empty` `rank_subsingleton'` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `Unique.instSubsingleton` `Cardinal.canonicallyOrderedAdd`
`collinear_iff_exists_forall_eq_smul_vadd` 📖	mathematical	—	`Collinear` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`Set.eq_empty_or_nonempty` `instIsEmptyFalse` `AddTorsor.nonempty` `collinear_iff_of_mem` `vadd_vadd` `sub_add_cancel`
`collinear_iff_finrank_le_one` 📖	mathematical	—	`Collinear` `Module.finrank` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module`	—	`collinear_iff_rank_le_one` `Nat.cast_one` `Cardinal.addLeftMono` `IsOrderedRing.toZeroLEOneClass` `Cardinal.isOrderedRing` `Cardinal.instCharZero` `Module.finrank_eq_rank` `IsNoetherianRing.strongRankCondition` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing`
`collinear_iff_not_affineIndependent` 📖	mathematical	—	`Collinear` `Set.range` `AffineIndependent` `DivisionRing.toRing`	—	`collinear_iff_finrank_le_one` `finiteDimensional_vectorSpan_range` `Finite.of_fintype` `finrank_vectorSpan_le_iff_not_affineIndependent` `Fintype.card_fin`
`collinear_iff_not_affineIndependent_of_ne` 📖	mathematical	—	`Collinear` `Set` `Set.instInsert` `Set.instSingletonSet` `AffineIndependent` `DivisionRing.toRing`	—	`Iff.not_left` `affineIndependent_iff_not_collinear_of_ne`
`collinear_iff_not_affineIndependent_set` 📖	mathematical	—	`Collinear` `Set` `Set.instInsert` `Set.instSingletonSet` `AffineIndependent` `DivisionRing.toRing` `Matrix.vecCons` `Matrix.vecEmpty`	—	`Iff.not_left` `affineIndependent_iff_not_collinear_set`
`collinear_iff_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`Collinear` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`IsNoetherianRing.strongRankCondition` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing` `Module.Free.of_divisionRing` `vsub_mem_vectorSpan` `eq_vadd_iff_vsub_eq` `vectorSpan_eq_span_vsub_set_right` `Submodule.span_le` `Set.subset_def` `SetLike.mem_coe` `Submodule.mem_span_singleton` `Set.mem_image` `vadd_vsub` `SetLike.le_def` `instIsConcreteLE`
`collinear_iff_rank_le_one` 📖	mathematical	—	`Collinear` `Cardinal` `Cardinal.instLE` `Module.rank` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module` `Cardinal.instOne`	—	—
`collinear_insert_iff_of_mem_affineSpan` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan`	`Collinear` `Set` `Set.instInsert`	—	`Collinear.eq_1` `vectorSpan_insert_eq_vectorSpan`
`collinear_insert_insert_insert_left_of_mem_affineSpan_pair` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set` `Set.instInsert` `Set.instSingletonSet`	`Collinear`	—	`Collinear.subset` `Set.insert_subset_insert` `collinear_insert_insert_insert_of_mem_affineSpan_pair`
`collinear_insert_insert_insert_of_mem_affineSpan_pair` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set` `Set.instInsert` `Set.instSingletonSet`	`Collinear`	—	`collinear_insert_iff_of_mem_affineSpan` `AffineSubspace.le_def'` `affineSpan_mono` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.subset_insert` `collinear_pair`
`collinear_insert_insert_of_mem_affineSpan_pair` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set` `Set.instInsert` `Set.instSingletonSet`	`Collinear`	—	`collinear_insert_iff_of_mem_affineSpan` `AffineSubspace.le_def'` `affineSpan_mono` `Set.subset_insert` `collinear_pair`
`collinear_insert_of_mem_affineSpan_pair` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set` `Set.instInsert` `Set.instSingletonSet`	`Collinear`	—	`collinear_insert_iff_of_mem_affineSpan` `collinear_pair`
`collinear_pair` 📖	mathematical	—	`Collinear` `Set` `Set.instInsert` `Set.instSingletonSet`	—	`collinear_iff_exists_forall_eq_smul_vadd` `Set.mem_singleton_iff` `Set.mem_insert_iff` `zero_smul` `zero_vadd` `one_smul` `vsub_vadd`
`collinear_singleton` 📖	mathematical	—	`Collinear` `Set` `Set.instSingletonSet`	—	`collinear_iff_rank_le_one` `vectorSpan_singleton` `rank_subsingleton'` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `Unique.instSubsingleton` `Cardinal.canonicallyOrderedAdd`
`collinear_triple_of_mem_affineSpan_pair` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set` `Set.instInsert` `Set.instSingletonSet`	`Collinear`	—	`Collinear.subset` `Set.insert_subset_insert` `collinear_insert_insert_insert_left_of_mem_affineSpan_pair`
`coplanar_empty` 📖	mathematical	—	`Coplanar` `Set` `Set.instEmptyCollection`	—	`Collinear.coplanar` `collinear_empty`
`coplanar_iff_finrank_le_two` 📖	mathematical	—	`Coplanar` `Module.finrank` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module`	—	`Nat.instAtLeastTwoHAddOfNat` `Cardinal.addLeftMono` `IsOrderedRing.toZeroLEOneClass` `Cardinal.isOrderedRing` `Cardinal.instCharZero` `Module.finrank_eq_rank` `IsNoetherianRing.strongRankCondition` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing`
`coplanar_insert_iff_of_mem_affineSpan` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan`	`Coplanar` `Set` `Set.instInsert`	—	`Coplanar.eq_1` `vectorSpan_insert_eq_vectorSpan`
`coplanar_of_fact_finrank_eq_two` 📖	mathematical	—	`Coplanar`	—	`coplanar_of_finrank_eq_two` `Fact.out`
`coplanar_of_finrank_eq_two` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	`Coplanar`	—	`FiniteDimensional.of_finrank_eq_succ` `coplanar_iff_finrank_le_two` `FiniteDimensional.finiteDimensional_submodule` `Submodule.finrank_le` `IsNoetherianRing.strongRankCondition` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing`
`coplanar_pair` 📖	mathematical	—	`Coplanar` `Set` `Set.instInsert` `Set.instSingletonSet`	—	`Collinear.coplanar` `collinear_pair`
`coplanar_singleton` 📖	mathematical	—	`Coplanar` `Set` `Set.instSingletonSet`	—	`Collinear.coplanar` `collinear_singleton`
`coplanar_triple` 📖	mathematical	—	`Coplanar` `Set` `Set.instInsert` `Set.instSingletonSet`	—	`Collinear.coplanar_insert` `collinear_pair`
`finiteDimensional_direction_affineSpan_image_of_finite` 📖	mathematical	—	`FiniteDimensional` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `AffineSubspace.direction` `affineSpan` `Set.image` `Submodule.addCommGroup` `Submodule.module`	—	`finiteDimensional_direction_affineSpan_of_finite` `Set.toFinite` `Finite.Set.finite_image` `Subtype.finite`
`finiteDimensional_direction_affineSpan_insert` 📖	mathematical	—	`FiniteDimensional` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `AffineSubspace.direction` `affineSpan` `Set` `Set.instInsert` `SetLike.coe` `AffineSubspace` `AffineSubspace.instSetLike` `Submodule.addCommGroup` `Submodule.module`	—	`finiteDimensional_vectorSpan_insert` `direction_affineSpan`
`finiteDimensional_direction_affineSpan_insert_set` 📖	mathematical	—	`FiniteDimensional` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `AffineSubspace.direction` `affineSpan` `Set` `Set.instInsert` `Submodule.addCommGroup` `Submodule.module`	—	`direction_affineSpan` `finiteDimensional_vectorSpan_insert_set`
`finiteDimensional_direction_affineSpan_of_finite` 📖	mathematical	—	`FiniteDimensional` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `AffineSubspace.direction` `affineSpan` `Submodule.addCommGroup` `Submodule.module`	—	`finiteDimensional_vectorSpan_of_finite` `direction_affineSpan`
`finiteDimensional_direction_affineSpan_range` 📖	mathematical	—	`FiniteDimensional` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `AffineSubspace.direction` `affineSpan` `Set.range` `Submodule.addCommGroup` `Submodule.module`	—	`finiteDimensional_direction_affineSpan_of_finite` `Set.finite_range`
`finiteDimensional_direction_affineSpan_singleton` 📖	mathematical	—	`FiniteDimensional` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `AffineSubspace.direction` `affineSpan` `Set` `Set.instSingletonSet` `Submodule.addCommGroup` `Submodule.module`	—	`direction_affineSpan` `finiteDimensional_vectorSpan_singleton`
`finiteDimensional_direction_map` 📖	mathematical	—	`FiniteDimensional` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `AffineSubspace.direction` `AffineSubspace.map` `Submodule.addCommGroup` `Submodule.module`	—	`RingHomSurjective.ids` `AffineSubspace.map_direction` `FiniteDimensional.instSubtypeMemSubmoduleMap`
`finiteDimensional_vectorSpan_image_of_finite` 📖	mathematical	—	`FiniteDimensional` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `Set.image` `Submodule.addCommGroup` `Submodule.module`	—	`finiteDimensional_vectorSpan_of_finite` `Set.toFinite` `Finite.Set.finite_image` `Subtype.finite`
`finiteDimensional_vectorSpan_insert` 📖	mathematical	—	`FiniteDimensional` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `Set` `Set.instInsert` `SetLike.coe` `AffineSubspace` `AffineSubspace.instSetLike` `Submodule.addCommGroup` `Submodule.module`	—	`direction_affineSpan` `affineSpan_insert_affineSpan` `Set.eq_empty_or_nonempty` `AffineSubspace.coe_eq_bot_iff` `AffineSubspace.bot_coe` `AffineSubspace.span_empty` `Set.instLawfulSingleton` `vectorSpan_singleton` `finiteDimensional_bot` `AffineSubspace.affineSpan_coe` `AffineSubspace.direction_affineSpan_insert` `Submodule.finiteDimensional_sup` `FiniteDimensional.span_singleton`
`finiteDimensional_vectorSpan_insert_set` 📖	mathematical	—	`FiniteDimensional` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `Set` `Set.instInsert` `Submodule.addCommGroup` `Submodule.module`	—	`direction_affineSpan` `affineSpan_insert_affineSpan` `finiteDimensional_vectorSpan_insert`
`finiteDimensional_vectorSpan_of_finite` 📖	mathematical	—	`FiniteDimensional` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `Submodule.addCommGroup` `Submodule.module`	—	`FiniteDimensional.span_of_finite` `Set.Finite.vsub`
`finiteDimensional_vectorSpan_range` 📖	mathematical	—	`FiniteDimensional` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `Set.range` `Submodule.addCommGroup` `Submodule.module`	—	`finiteDimensional_vectorSpan_of_finite` `Set.finite_range`
`finiteDimensional_vectorSpan_singleton` 📖	mathematical	—	`FiniteDimensional` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `Set` `Set.instSingletonSet` `Submodule.addCommGroup` `Submodule.module`	—	`finiteDimensional_vectorSpan_of_finite` `Set.finite_singleton`
`finite_of_fin_dim_affineIndependent` 📖	mathematical	`AffineIndependent` `DivisionRing.toRing`	`Finite`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Finite.of_subsingleton` `Set.Finite.finite_of_compl` `Nontrivial.to_nonempty` `Set.finite_singleton` `Set.finite_coe_iff` `LinearIndependent.finite_of_isNoetherian` `IsNoetherian.iff_fg` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `affineIndependent_iff_linearIndependent_vsub`
`finite_set_of_fin_dim_affineIndependent` 📖	mathematical	`AffineIndependent` `DivisionRing.toRing` `Set.Elem`	`Set.Finite`	—	`Set.toFinite` `finite_of_fin_dim_affineIndependent`
`finrank_vectorSpan_image_finset_le` 📖	mathematical	`Finset.card`	`Module.finrank` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.image` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module`	—	`Finset.image_nonempty` `Finset.card_pos` `vectorSpan_eq_span_vsub_finset_right_ne` `le_trans` `finrank_span_finset_le_card` `IsNoetherianRing.strongRankCondition` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing` `Finset.card_image_of_injective` `vsub_left_injective` `Finset.card_erase_of_mem` `tsub_le_iff_right` `Nat.instOrderedSub` `Finset.card_image_le`
`finrank_vectorSpan_insert_le` 📖	mathematical	—	`Module.finrank` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `Set` `Set.instInsert` `SetLike.coe` `AffineSubspace` `AffineSubspace.instSetLike` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module` `AffineSubspace.direction`	—	`direction_affineSpan` `affineSpan_insert_affineSpan` `Set.eq_empty_or_nonempty` `AffineSubspace.coe_eq_bot_iff` `AffineSubspace.bot_coe` `AffineSubspace.span_empty` `AffineSubspace.direction_bot` `finrank_bot` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `zero_add` `Set.instLawfulSingleton` `vectorSpan_singleton` `zero_le_one'` `Nat.instZeroLEOneClass` `AffineSubspace.affineSpan_coe` `AffineSubspace.direction_affineSpan_insert` `add_comm` `LE.le.trans` `Submodule.finrank_add_le_finrank_add_finrank` `FiniteDimensional.span_singleton` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `finrank_le_one` `IsNoetherianRing.strongRankCondition` `PrincipalIdealRing.isNoetherianRing` `DivisionSemiring.isPrincipalIdealRing` `Submodule.mem_span_singleton_self` `Submodule.mem_span_singleton` `vectorSpan_mono` `Set.subset_insert` `Submodule.finiteDimensional_of_le` `Module.finrank_of_infinite_dimensional` `zero_le_one`
`finrank_vectorSpan_insert_le_set` 📖	mathematical	—	`Module.finrank` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `Set` `Set.instInsert` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module`	—	`direction_affineSpan` `affineSpan_insert_affineSpan` `finrank_vectorSpan_insert_le`
`finrank_vectorSpan_le_iff_not_affineIndependent` 📖	mathematical	`Fintype.card`	`Module.finrank` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `Set.range` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module` `AffineIndependent`	—	`not_iff_comm` `affineIndependent_iff_not_finrank_vectorSpan_le`
`finrank_vectorSpan_range_add_one_le` 📖	mathematical	—	`Module.finrank` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `Set.range` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module` `Fintype.card`	—	`le_tsub_iff_right` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Fintype.card_pos` `finrank_vectorSpan_range_le` `tsub_add_cancel_of_le`
`finrank_vectorSpan_range_le` 📖	mathematical	`Fintype.card`	`Module.finrank` `Submodule` `Ring.toSemiring` `DivisionRing.toRing` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `Set.range` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Submodule.addCommMonoid` `Submodule.module`	—	`Set.image_univ` `Finset.coe_univ` `Finset.coe_image` `finrank_vectorSpan_image_finset_le` `Finset.card_univ`
`ne₁₂_of_not_collinear` 📖	—	`Collinear` `Set` `Set.instInsert` `Set.instSingletonSet`	—	—	`Set.insert_eq_of_mem`
`ne₁₃_of_not_collinear` 📖	—	`Collinear` `Set` `Set.instInsert` `Set.instSingletonSet`	—	—	`Set.insert_eq_of_mem`
`ne₂₃_of_not_collinear` 📖	—	`Collinear` `Set` `Set.instInsert` `Set.instSingletonSet`	—	—	`Set.insert_eq_of_mem`

---

← Back to Index