Zulip Chat Archive
Stream: mathlib4
Topic: additivized IsConj
Eric Rodriguez (Jun 26 2023 at 17:10):
Not that I think it's ever a useful concept, but docs#IsConj does not have an additive version.
Eric Rodriguez (Jun 26 2023 at 17:13):
Meanwhile, docs#SemiconjBy seems to be. I think we do have other "mathematically useless" additivizations, so where do we draw the line?
Eric Rodriguez (Jun 26 2023 at 17:13):
For example, I think centralizers are additivized.
Yaël Dillies (Jun 26 2023 at 17:14):
I found myself needing is_add_conj a while back, so I would be happy for it to be added (ha!).
Eric Rodriguez (Jun 26 2023 at 17:14):
Out of curiosity, where?
Yaël Dillies (Jun 26 2023 at 17:15):
Understand: I didn't want to use it directly, but rather it was used to prove lemmas whose additive version I wanted.
Last updated: Dec 20 2023 at 11:08 UTC