Theorems · Theorem · geometry

AffineMap.homothety_mul_apply

∀ {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₁ r₂ : k) (p : P1),
  (AffineMap.homothety c (r₁ * r₂)) p = (AffineMap.homothety c r₁) ((AffineMap.homothety c r₂) p)

Defined in

Mathlib.LinearAlgebra.AffineSpace.AffineMap

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupAddTorsorModule