Main results

The main results that the formalization.yaml of FormalFrontier/morphism-properties lists under status.main_results at commit 1666ed81, each that the scan finds declared in the file the yaml gives, with its line. They are listed here, not made articles: in several Formal Frontier libraries this list is close to the whole API. The notes are the yaml's.

Declaration	Kind	Where	Note
CategoryTheory.CostructuredArrow.isDenseAt_toOver	theorem	MorphismProperties/Density.lean, line 44
CategoryTheory.CostructuredArrow.isDense_toOver	instance	MorphismProperties/Density.lean, line 67
CategoryTheory.MorphismProperty.isStableUnderBaseChange_either_iff	theorem	MorphismProperties/RelativeBaseChange.lean, line 73
CategoryTheory.MorphismProperty.pullbackLift_fst_snd_of_intersection_of_postcomp	theorem	MorphismProperties/RelativeBaseChange.lean, line 138
CategoryTheory.MorphismProperty.Over.pullbackOfIntersectionOfPostcomp	def	MorphismProperties/OverPullback.lean, line 50
CategoryTheory.MorphismProperty.Over.pullbackPairing_map_mem_of_relative	theorem	MorphismProperties/PullbackPairing.lean, line 294

Quoted from the main results in formalization.yaml of FormalFrontier/morphism-properties at commit 1666ed81, Apache-2.0.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.