Theorem AlgebraicGeometry.Scheme.Hom.appIso_hom'

Modification history

2024-07-21 21:46

Mathlib/AlgebraicGeometry/OpenImmersion.lean

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

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