Theorem AlgebraicGeometry.Scheme.inv_val_c_app_top

Modification history

2024-06-25 05:48

Mathlib/AlgebraicGeometry/Scheme.lean

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

Deleted AlgebraicGeometry.Scheme.inv_val_c_app_top View on Github →

2023-11-12 21:46

Mathlib/AlgebraicGeometry/Scheme.lean

perf(AlgebraicGeometry): Fix slow and bad proofs (#7747) …

Added AlgebraicGeometry.Scheme.inv_val_c_app_top View on Github →