Module

Finite.lean

Nyll.SchemeTheory.Pi1.Morphisms.Finite

1 declaration indexed from sourceView source ↗

Module documentation

Finite morphisms satisfy cancellation after postcomposition by a finite morphism.

Imports1

Imported by2

instance

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
universe u
open CategoryTheory Limits MorphismProperty
namespace AlgebraicGeometry
namespace IsFinite

Lean source · full declaration

instance : HasOfPostcompProperty @IsFinite @IsFinite where
  of_postcomp f g _ _ := .of_comp f g