instMonoid — Mathlib

English

The map that sends a continuous R-algebra endomorphism to its underlying AlgHom is a monoid homomorphism from End_R(A) to AlgHom_R(A,A).

Русский

Отображение, переводящее непрерывный R-алгебра-гомоморфизм в соответствующий AlgHom, является гомоморфизмом моноидов End_R(A) → AlgHom_R(A,A).

LaTeX

$$toAlgHomMonoidHom : (A →A[R] A) →* A →ₐ[R] A$$

Lean4

instance : Monoid (A →A[R] A) where
  mul_one _ := ext fun _ => rfl
  one_mul _ := ext fun _ => rfl
  mul_assoc _ _ _ := ext fun _ => rfl

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