Theorems · Theorem · geometry

Projectivization.cross_mk

∀ {F : Type u_1} [inst : Field F] [inst_1 : DecidableEq F] {v w : Fin 3 → F} (hv : v ≠ 0) (hw : w ≠ 0),
  (Projectivization.mk F v hv).cross (Projectivization.mk F w hw) =
    if h : (crossProduct v) w = 0 then Projectivization.mk F v hv else Projectivization.mk F ((crossProduct v) w) h

Defined in

Mathlib.LinearAlgebra.Projectivization.Constructions

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldDecidableEq