Theorem AlgebraicGeometry.morphismRestrict_homOfLE

Modification history

2026-05-27 15:58

Mathlib/AlgebraicGeometry/Restrict.lean

feat(AlgebraicGeometry/Restrict): a few more restriction lemmas (#39442) …

Added AlgebraicGeometry.morphismRestrict_homOfLE View on Github →