toProd_surjective

Mathlib.GroupTheory.Coprod.Basic

URI: https://scilib.ai/kg/mathlib#Monoid.Coprod.toProd_surjective

← MathLib Explorer

English

The map toProd: G ∗ H → G × H is surjective.

Русский

Отображение toProd: G ∗ H → G × H сюръективно.

LaTeX

$$$ \text{Surjective}(\mathrm{toProd}: G \ast H \to G \times H). $$$

Lean4

@[to_additive toProd_surjective]
theorem toProd_surjective : Surjective (toProd : M ∗ N →* M × N) := fun x =>
  ⟨inl x.1 * inr x.2, by rw [map_mul, toProd_apply_inl, toProd_apply_inr, Prod.fst_mul_snd]⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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