Mathlib v3 is deprecated. Go to Mathlib v4

Theorem algebraic_geometry.is_open_immersion.app_eq_inv_app_app_of_comp_eq

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.is_open_immersion.app_eq_inv_app_app_of_comp_eqView on Github →