refactor(algebra/*): reduce use of old_structure_cmd in sub-objects #9774
Conversation
semorrison
added
WIP
| @@ -36,8 +41,23 @@ variables [comm_semiring R] | |||
| variables [semiring A] [algebra R A] [semiring B] [algebra R B] [semiring C] [algebra R C] | |||
| include R | |||
|
|
|||
| /-- An alternative constructor for subalgebras which does not require separate proofs that | |||
| the subalgebra contains 0 and 1. -/ | |||
| def mk' (s : set A) | |||
There was a problem hiding this comment.
| def mk' (s : set A) | |
| @[simp] def mk' (s : set A) |
else you have to repeat all the coe_mk-type defs for coe_mk'
There was a problem hiding this comment.
It seems we don't have coe_mk-type defs for subalgebra in any case, and the lack of them (or of coe_mk' lemmas) is not currently hurting anything, so perhaps this is a separate issue to this PR?
| let s : subalgebra R (tensor_algebra R M) := { | ||
| carrier := C, | ||
| mul_mem' := h_mul, | ||
| add_mem' := h_add, | ||
| algebra_map_mem' := h_grade0, }, | ||
| let s : subalgebra R (tensor_algebra R M) := subalgebra.mk' C h_add h_mul h_grade0, |
There was a problem hiding this comment.
I'd argue this is less readable than it was before, and have mentioned in on Zulip. I'm not sure we can justify removing old_structure_cmd simply because it uses the word "old" ;).
There was a problem hiding this comment.
See response on zulip. I think "simply because it uses the word "old"" doesn't quite get at it. :-)
github-actions
bot
added
the
blocked-by-other-PR
github-actions
bot
removed
awaiting-CI
|
🎉 Great news! Looks like all the dependencies have been resolved: 💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
github-actions
bot
added
the
merge-conflict
github-actions
bot
removed
the
merge-conflict
|
I've cherrypicked out a few of the "stability" changes to downstream proofs, and made them as separate PRs, so I'll close this for now. |
This removes the use of
old_structure_cmdinsub(semi)ring,subalgebra,subfield, andintermediate_field.Still to go is
(lie_)submoduleandsub_mul_action; not sure yet whether that will go in this PR or separately.