Theorem AlgebraicGeometry.Scheme.inv_app_top

Modification history

2024-11-24 13:54

Mathlib/AlgebraicGeometry/Scheme.lean

chore(AlgebraicGeometry) add `Scheme.Hom.appTop` (#19130) …

Deleted AlgebraicGeometry.Scheme.inv_app_top View on Github →

2024-06-25 05:48

Mathlib/AlgebraicGeometry/Scheme.lean

refactor(AlgebraicGeometry): Use `Scheme.Hom.app` as simp normal form (#14031)

Added AlgebraicGeometry.Scheme.inv_app_top View on Github →