diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean index e96aae3..dd35253 100644 --- a/CommAlg/final_poly_type.lean +++ b/CommAlg/final_poly_type.lean @@ -5,7 +5,6 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic set_option maxHeartbeats 0 macro "ls" : tactic => `(tactic|library_search) --- From Kyle : New tactic "obviously" -- From Kyle : New tactic "obviously" macro "obviously" : tactic => `(tactic| (