Theorems · Definition · geometry

Coplanar

(k : Type u_1) →
  {V : Type u_2} →
    {P : Type u_3} → [inst : DivisionRing k] → [inst_1 : AddCommGroup V] → [Module k V] → [AddTorsor V P] → Set P → Prop

A set of points is coplanar if their vectorSpan has dimension at most 2.

Defined in: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Cited by: 15 results in Mathlib
Foundations: Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: DivisionRing AddCommGroup Module AddTorsor

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Modulestatement and proof · cited by 20,661
AddCommGroupstatement and proof · cited by 12,871
AddTorsorstatement and proof · cited by 1,657
DivisionRingstatement and proof · cited by 1,062
Module.rankproof · cited by 496
vectorSpanproof · cited by 123

Cited by17

Results whose statement or proof uses this declaration.

Collinear.coplanarstatement · cited by 3
coplanar_iff_finrank_le_twostatement and proof · cited by 3
coplanar_of_fact_finrank_eq_twostatement · cited by 2
Coplanar.finiteDimensional_vectorSpanstatement and proof · cited by 1
Coplanar.subsetstatement and proof · cited by 1
Collinear.coplanar_insertstatement · cited by 1
coplanar_emptystatement · cited by 1
coplanar_of_finrank_eq_twostatement · cited by 1
coplanar_pairstatement · cited by 1
coplanar_singletonstatement · cited by 1
EuclideanGeometry.Concyclic.Coplanarstatement · cited by 1
Coplanar.finiteDimensional_direction_affineSpanstatement and proof · cited by 0