mathlib3
[Merged by Bors] - chore(algebraic_geometry/Scheme): remove @[simps] from Spec
#19188

Closed

[Merged by Bors] - chore(algebraic_geometry/Scheme): remove @[simps] from Spec #19188

kim-em wants to merge 6 commits into master from Spec_simps

chore(algebraic_geometry/Scheme): remove @[simps] from Spec

8bbef1bb

kim-em added awaiting-review

kim-em added awaiting-CI

kim-em requested a review 2 years ago

eric-wieser commented on 2023-06-14

Update src/algebraic_geometry/properties.lean

cbdc32ea

kim-em commented on 2023-06-14

github-actions removed awaiting-CI

add some simp lemmas

8d91580f

github-actions added modifies-synchronized-file

actually write them

ad7c148e

eric-wieser approved these changes on 2023-06-15

leanprover-community-bot-assistant added delegated

leanprover-community-bot-assistant removed awaiting-review

eric-wieser commented on 2023-06-15

github-actions added ready-to-merge

revert addition of lemmas that only cause problems

b988c901

doc comment

d87e8f24

jcommelin approved these changes on 2023-06-15

bors changed the title ~~chore(algebraic_geometry/Scheme): remove @[simps] from Spec~~ [Merged by Bors] - chore(algebraic_geometry/Scheme): remove @[simps] from Spec 2 years ago

bors closed this 2 years ago

bors deleted the Spec_simps branch 2 years ago

Reviewers

jcommelin

eric-wieser

erdOne

Assignees

No one assigned

Labels

ready-to-merge delegated modifies-synchronized-file

Milestone

No milestone

mathlib3 [Merged by Bors] - chore(algebraic_geometry/Scheme): remove @[simps] from Spec #19188 Closed

[Merged by Bors] - chore(algebraic_geometry/Scheme): remove @[simps] from Spec #19188

mathlib3
[Merged by Bors] - chore(algebraic_geometry/Scheme): remove @[simps] from Spec
#19188

Closed