Theorems · Theorem · geometry

AffineBasis.affineIndependent_of_toMatrix_right_inv

∀ {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) {ι' : Type u_1} [inst_4 : Fintype ι] [Finite ι']
  [inst_6 : DecidableEq ι'] (p : ι' → P) {A : Matrix ι ι' k}, b.toMatrix p * A = 1 → AffineIndependent k p

Given a family of points p : ι' → P and an affine basis b, if the matrix whose rows are the coordinates of p with respect b has a right inverse, then p is affine independent.

Defined in

Mathlib.LinearAlgebra.AffineSpace.Matrix

Cited by

1 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupAddTorsorRingModuleFintypeFiniteDecidableEq