Theorem CategoryTheory.homIsOver_of_isOverTower

Modification history

2024-11-06 12:25
Mathlib/CategoryTheory/Comma/OverClass.lean
feat(AlgebraicGeometry): typeclasses for `S`-schemes (#18321)
Added CategoryTheory.homIsOver_of_isOverTowerView on Github →