Theorems · Theorem · algebraic geometry
AlgebraicGeometry.AffineSpace.reindex_id
∀ {n : Type u} (S : AlgebraicGeometry.Scheme),
AlgebraicGeometry.AffineSpace.reindex id S = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.AffineSpace n S)- Defined in
- Mathlib.AlgebraicGeometry.AffineSpace
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 175 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement · cited by 32,603
- CategoryTheory.CategoryStruct.idstatement and proof · cited by 6,235
- AlgebraicGeometry.Schemestatement and proof · cited by 2,540
- CategoryTheory.overproof · cited by 76
- AlgebraicGeometry.AffineSpacestatement and proof · cited by 51
- AlgebraicGeometry.AffineSpace.coordproof · cited by 19
- CategoryTheory.comp_overproof · cited by 14
- AlgebraicGeometry.AffineSpace.reindexstatement and proof · cited by 9
- AlgebraicGeometry.AffineSpace.hom_extproof · cited by 8
- AlgebraicGeometry.AffineSpace.reindex_appTop_coordproof · cited by 3
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.