Theorems · Theorem · geometry

AffineMap.homothety_def

∀ {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [inst : CommRing k] [inst_1 : AddCommGroup V1]
  [inst_2 : AddTorsor V1 P1] [inst_3 : Module k V1] (c : P1) (r : k),
  AffineMap.homothety c r = r • (AffineMap.id k P1 -ᵥ AffineMap.const k P1 c) +ᵥ AffineMap.const k P1 c

Defined in

Mathlib.LinearAlgebra.AffineSpace.AffineMap

Cited by

0 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Quot.sound

Assumes

CommRingAddCommGroupAddTorsorModule