Theorem AlgebraicGeometry.Spec.topObj_forget

Modification history

2025-02-12 15:26

Mathlib/AlgebraicGeometry/Spec.lean

refactor(*): get rid of `(forget _).obj` and `(forget _).map` (#21727) …

Modified AlgebraicGeometry.Spec.topObj_forget View on Github →

2024-05-21 04:23

Mathlib/AlgebraicGeometry/Spec.lean

feat: simp lemma for coercions in TopCat (#12956) …

Added AlgebraicGeometry.Spec.topObj_forget View on Github →