ι_appIso

Mathlib.AlgebraicGeometry.Restrict

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.Opens.ι_appIso

English

Additional helper lemmas for equivalence in SpecToEquivOfField construction.

Русский

Дополнительные вспомогательные леммы для эквивалентности в конструкции SpecToEquivOfField.

LaTeX

$$SpecToEquivOfField_eq_iff and related simp lemmas$$

Lean4

@[simp]
theorem ι_appIso (V) : U.ι.appIso V = Iso.refl _ :=
  X.ofRestrict_appIso _ _

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

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

Разделы

Аффилиация

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