Def AlgebraicGeometry.Scheme.Hom.appIso

Modification history

2024-07-21 21:46

Mathlib/AlgebraicGeometry/OpenImmersion.lean

refactor(AlgebraicGeometry): Promote `invApp` to an iso. (#14868)

Added AlgebraicGeometry.Scheme.Hom.appIso View on Github →