ofQuotient_isPresentation — Mathlib

English

The object built from quotients is itself a presentation; the bijective correspondence ensures the presentation property.

Русский

Объект, построенный из квотентов, сам по себе является презентацией; биекция обеспечивает это свойство презентации.

LaTeX

$$$$ \\text{ofQuotient\_isPresentation} \\;:\\; (\\mathrm{ofQuotient\\, relations}).IsPresentation $$$$

Lean4

theorem ofQuotient_isPresentation : (ofQuotient relations).IsPresentation where
  bijective := by simpa only [ofQuotient_fromQuotient, LinearMap.id_coe] using Function.bijective_id

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