Theorem AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop

Modification history

2026-06-01 14:37

Mathlib/AlgebraicGeometry/AffineSpace.lean

perf(AlgebraicGeometry): specialize index type in `AffineSpace` to `Type u` (#39970) …

Modified AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop View on Github →

2024-11-24 13:54

Mathlib/AlgebraicGeometry/AffineSpace.lean

chore(AlgebraicGeometry) add `Scheme.Hom.appTop` (#19130) …

Added AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop View on Github →