snd

Mathlib.Topology.Algebra.Algebra

URI: https://scilib.ai/kg/mathlib#ContinuousAlgHom.snd

English

fst is the continuous R-algebra homomorphism sending (a,b) to a.

Русский

fst — непрерывный R-алгебра-гомоморфизм, отправляющий (a,b) в a.

LaTeX

$$def fst : A × B →A[R] A$$

Lean4

/-- `Prod.snd` as a `ContinuousAlgHom`. -/
def snd : A × B →A[R] B where
  cont := continuous_snd
  toAlgHom := AlgHom.snd R A B

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

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

Разделы

Аффилиация

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