Theorem AlgebraicGeometry.Scheme.Hom.appIso_inv_app_apply'

Modification history

2025-02-11 15:35

Mathlib/AlgebraicGeometry/OpenImmersion.lean

refactor(*): get rid of last `HasForget.instFunLike` instances (#21725) …

Deleted AlgebraicGeometry.Scheme.Hom.appIso_inv_app_apply'View on Github →

2024-12-13 13:44

Mathlib/AlgebraicGeometry/OpenImmersion.lean

refactor(Algebra/Category/Ring): make morphisms a structure (#19757) …

Added AlgebraicGeometry.Scheme.Hom.appIso_inv_app_apply'View on Github →