Theorems · Definition · geometry

Projectivization.Independent.casesOn

∀ {ι : Type u_1} {K : Type u_2} {V : Type u_3} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {motive : (a : ι → Projectivization K V) → Projectivization.Independent a → Prop} {a : ι → Projectivization K V}
  (t : Projectivization.Independent a),
  (∀ (f : ι → V) (hf : ∀ (i : ι), f i ≠ 0) (hl : LinearIndependent K f),
      motive (fun i => Projectivization.mk K (f i) ⋯) ⋯) →
    motive a t

Defined in

Mathlib.LinearAlgebra.Projectivization.Independence

Cited by

2 results in Mathlib

Foundations

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

Assumes

DivisionRingAddCommGroupModule