Idempotent ring elements #2105
Idempotent ring elements #2105
Conversation
Signed-off-by: Ali Caglayan <[email protected]> <!-- ps-id: d7fcadf7-90ae-4f92-8dd4-bb25a7aa8114 -->
| Proof. | ||
| snrapply Build_IsOrthogonal. | ||
| - exact (rng_idem_orth' (R:=R)). | ||
| - exact (rng_idem_orth (R:=R)). | ||
| Defined. |
There was a problem hiding this comment.
Does it work to replace this proof with := isorthogonal_swap R e f r.?
There was a problem hiding this comment.
Not quite. I tried it again and it still doesn't work. I also thought something like this should work but I couldn't work it out.
There was a problem hiding this comment.
I wonder if it's because of the proofs of idempotency that are carried along? (Incidentally, they aren't used in any way, but I guess it makes sense to keep them.) In any case, this isn't worth worrying about.
Co-authored-by: Dan Christensen <[email protected]>
Co-authored-by: Dan Christensen <[email protected]>
| Proof. | ||
| snrapply Build_IsOrthogonal. | ||
| - exact (rng_idem_orth' (R:=R)). | ||
| - exact (rng_idem_orth (R:=R)). | ||
| Defined. |
There was a problem hiding this comment.
I wonder if it's because of the proofs of idempotency that are carried along? (Incidentally, they aren't used in any way, but I guess it makes sense to keep them.) In any case, this isn't worth worrying about.
Co-authored-by: Dan Christensen <[email protected]>
Co-authored-by: Dan Christensen <[email protected]>
Co-authored-by: Dan Christensen <[email protected]>
|
Forgot to merge this the other day. |
Addresses first part of #2009. I can't recall any other identities to do with idempotent ring elements.