Def algebraic_geometry.Scheme.hom.inv_app

Modification history

2022-11-09 03:23
src/algebraic_geometry/open_immersion.lean
feat(algebraic_geometry/open_immersion): `is_open_immersion.lift_app` (#17186)
Added algebraic_geometry.Scheme.hom.inv_appView on Github →