homothetyUnitsMulHom — Mathlib

English

Fixing a point p in an affine space, sending a scalar unit t to the homothety about p defines a group hom from units of the scalar ring to affine automorphisms.

Русский

Фиксируя точку p в афинном пространстве, отображение единиц кольца на гомотетию вокруг p образует гомоморфизм групп единиц скаляров в аффинные преобразования.

LaTeX

$$homothetyUnitsMulHom(p) : Units(R) →* P ≃ᵃ[R] P$$

Lean4

/-- 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. -/
def homothetyUnitsMulHom (p : P) : Rˣ →* P ≃ᵃ[R] P :=
  equivUnitsAffineMap.symm.toMonoidHom.comp <| Units.map (AffineMap.homothetyHom p)

Похожие утверждения