coe_eq_id — Mathlib

English

The coe of a composition of continuous algebra homomorphisms equals the composition of the coes.

Русский

Сопряжение композиции непрерывных гомоморфизмов равно композиции их сопряжений.

LaTeX

$$coe (h ∘ f) = (coe h) ∘ (coe f)$$

Lean4

@[simp, norm_cast]
theorem coe_eq_id {f : A →A[R] A} : (f : A →ₐ[R] A) = AlgHom.id R A ↔ f = ContinuousAlgHom.id R A := by
  rw [← coe_id, coe_inj]

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