coe_homothetyUnitsMulHom_eq_homothetyHom_coe

English

Expressing the equality of function actions between the scalar units and the affine map homothety.

Русский

Выражение эквивалентности действий через единицы скаляров и гомотетию.

LaTeX

$$((↑) : P →ᵃ P) ∘ homothetyUnitsMulHom(p) = AffineMap.homothetyHom(p) ∘ ((↑) : Units(R) → R)$$

Lean4

@[simp]
theorem coe_homothetyUnitsMulHom_eq_homothetyHom_coe (p : P) :
    ((↑) : (P ≃ᵃ[R] P) → P →ᵃ[R] P) ∘ homothetyUnitsMulHom p = AffineMap.homothetyHom p ∘ ((↑) : Rˣ → R) :=
  funext fun _ => rfl

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