free_congr_left

Mathlib.Combinatorics.SimpleGraph.Copy

URI: https://scilib.ai/kg/mathlib#SimpleGraph.free_congr_left

English

If e₁ : A ≃g B, then A.Free C ↔ B.Free C.

Русский

Если e₁: A ≃g B, то A.Free C эквивалентно B.Free C.

LaTeX

$$e₁ : A ≃g B → (A.Free C ↔ B.Free C)$$

Lean4

theorem free_congr_left (e₁ : A ≃g B) : A.Free C ↔ B.Free C :=
  free_congr e₁ .refl

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

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

Разделы

Аффилиация

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