Theorems · Theorem · geometry

lineMap_slope_slope_sub_div_sub

∀ {k : Type u_1} {E : Type u_2} {PE : Type u_3} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E]
  [inst_3 : AddTorsor E PE] (f : k → PE) (a b c : k),
  a ≠ c → (AffineMap.lineMap (slope f a b) (slope f b c)) ((c - b) / (c - a)) = slope f a c

slope f a c is an affine combination of slope f a b and slope f b c. This version uses lineMap to express this property.

Defined in

Mathlib.LinearAlgebra.AffineSpace.Slope

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldAddCommGroupModuleAddTorsor