Theorems · Definition · geometry

AffineEquiv.homothetyUnitsMulHom

{R : Type u_10} →
  {V : Type u_11} →
    {P : Type u_12} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup V] → [inst_2 : Module R V] → [inst_3 : AddTorsor V P] → P → Rˣ →* P ≃ᵃ[R] P

Fixing a point in affine space, homothety about this point gives a group homomorphism from (the centre of) the units of the scalars into the group of affine equivalences.

Defined in

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleAddTorsor