comp_iff

Mathlib.AlgebraicGeometry.Morphisms.Separated

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.IsAffineHom.comp_iff

English

Same as above: IsAffineHom (f ≫ g) is equivalent to IsAffineHom f when [IsAffineHom g].

Русский

Та же самая вещь: IsAffineHom (f ≫ g) эквивалентно IsAffineHom f при условии [IsAffineHom g].

LaTeX

$$$IsAffineHom(f \circ g) \iff IsAffineHom(f)$, при условии [IsAffineHom g].$$

Lean4

theorem comp_iff [IsAffineHom g] : IsAffineHom (f ≫ g) ↔ IsAffineHom f :=
  ⟨fun _ ↦ .of_comp f g, fun _ ↦ inferInstance⟩

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

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

Разделы

Аффилиация

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