ofLocalizationSpanTarget

Mathlib.RingTheory.RingHom.Etale

URI: https://scilib.ai/kg/mathlib#RingHom.Etale.ofLocalizationSpanTarget

English

Étale morphisms satisfy a localization-span target property.

Русский

Этale-морфизм удовлетворяет свойству локализационного спана цели.

LaTeX

$$$\\operatorname{OfLocalizationSpanTarget}(Etale)$$$

Lean4

theorem ofLocalizationSpanTarget : OfLocalizationSpanTarget Etale :=
  propertyIsLocal.ofLocalizationSpanTarget

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

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

Разделы

Аффилиация

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