[Merged by Bors] - fix(Algebra/IndicatorFunction): minor fixes#6640
[Merged by Bors] - fix(Algebra/IndicatorFunction): minor fixes#6640
Conversation
- Fix name in docstrings. - Use `Type*` in `variable`, explicitly use `Sort*`. - Use `to_additive` to generate the additive version. - Drop pattern matching. - Add `Set.mulIndicator_diff'`, the multiplicative version of `Set.indicator_diff`.
| open Function | ||
|
|
||
| variable {α β ι M N : Type _} | ||
| variable {α β ι M N : Type*} |
There was a problem hiding this comment.
I'm surprised it even worked with the latest changes!
| @[to_additive indicator_diff] | ||
| theorem mulIndicator_diff' (h : s ⊆ t) (f : α → G) : |
There was a problem hiding this comment.
Could you do the same for compl?
Also, it's a bit annoying if the primes in the name are mixed up (IIUC with your change we would have mulIndicator_diff <-> indicator_diff' and mulIndicator_diff' <-> indicator_diff), should we make sure that they match up (in a follow up PR since that's probably going to touch a lot of files) or is it expected that the "default" lemma is different?
There was a problem hiding this comment.
It seems that we mostly use a * b⁻¹ for groups, a / b for fields, and a - b for additive groups.
There was a problem hiding this comment.
Okay that makes sense. Let's keep it like that then.
|
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
- Fix name in docstrings. - Use `Type*` in `variable`, explicitly use `Sort*`. - Use `to_additive` to generate the additive version. - Drop pattern matching. - Add `Set.mulIndicator_diff'`, the multiplicative version of `Set.indicator_diff`.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
Type*invariable, explicitly useSort*.to_additiveto generate the additive version.Set.mulIndicator_diff',the multiplicative version of
Set.indicator_diff.