isMulFreimanHom_id

Mathlib.Combinatorics.Additive.FreimanHom

URI: https://scilib.ai/kg/mathlib#isMulFreimanHom_id

← MathLib Explorer

English

The identity map on A1 ⊆ A2 is a FreimanHom from A1 to A2 of any order n.

Русский

Идентичное отображение на A1 ⊆ A2 является FreimanHom порядка n от A1 к A2.

LaTeX

$$isMulFreimanHom_id (hA) : IsMulFreimanHom n A1 A2 id$$

Lean4

@[to_additive]
theorem isMulFreimanHom_id (hA : A₁ ⊆ A₂) : IsMulFreimanHom n A₁ A₂ id
    where
  mapsTo := hA
  map_prod_eq_map_prod s t _ _ _ _ h := by simpa using h

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

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

Разделы

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

Аффилиация

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