coe

Mathlib.Topology.Algebra.Algebra.Equiv

URI: https://scilib.ai/kg/mathlib#ContinuousAlgEquiv.coe

English

The coercion from a continuous algebra equivalence to a continuous algebra homomorphism is well-defined.

Русский

Связь перехода из непрерывного алгебраического эквивалента в непрерывное алгебраическое гомоморфизм корректна.

LaTeX

$$coe : (A ≃A[R] B) → A →A[R] B$$

Lean4

instance coe : Coe (A ≃A[R] B) (A →A[R] B) :=
  ⟨toContinuousAlgHom⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru