[Merged by Bors] - refactor(algebra/group/basic): add extra typeclasses for negation #11960
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
eric-wieser
force-pushed
the
eric-wieser/monoid_with_neg
branch
from
93d8381
to
dc16362
Compare
eric-wieser
force-pushed
the
eric-wieser/monoid_with_neg
branch
from
ccd4e22
to
ff123b3
Compare
|
Please list all new classes in the commit message. |
jsm28
reviewed
Feb 10, 2022
eric-wieser
added
awaiting-CI
That was always my plan once I hit most of the lemmas I planned to move. |
urkud
reviewed
Feb 10, 2022
eric-wieser
commented
Feb 10, 2022
github-actions
bot
removed
the
awaiting-CI
urkud
reviewed
Feb 15, 2022
urkud
reviewed
Feb 15, 2022
test/matrix.lean
Outdated
| -/ | ||
| -- Previously we could do `simp [matrix.det_succ_row_zero, fin.sum_univ_succ]`, but that now times | ||
| -- out. | ||
| rw det_fin_three, |
There was a problem hiding this comment.
I think that this example was here to show how to compute the determinant of any matrix, not only 3*3. Can we fix the timeout in some other way?
There was a problem hiding this comment.
I don't really understand why the timeout is happening I'm afraid. Do you think we need to get to the bottom of it before merging, or are you ok with just going ahead with the change anyway.
|
Otherwise LGTM |
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
eric-wieser
commented
Feb 15, 2022
…prover-community/mathlib into eric-wieser/monoid_with_neg
|
bors merge |
github-actions
bot
added
the
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Feb 16, 2022
…1960) The new typeclasses are: * `has_involutive_inv R`, stating that `(r⁻¹)⁻¹ = r` (instances: `group`, `group_with_zero`, `ennreal`, `set`, `submonoid`) * `has_involutive_neg R`, stating that `- -r = r` (instances: `add_group`, `ereal`, `module.ray`, `ray_vector`, `set`, `add_submonoid`, `jordan_decomposition`) * `has_distrib_neg R`, stating that `-a * b = a * -b = -(a * b)` (instances: `ring`, `units`, `unitary`, `special_linear_group`, `GL_pos`) While the original motivation only concerned the two `neg` typeclasses, the `to_additive` machinery forced the introduction of `has_involutive_inv`, which turned out to be used in more places than expected. Adding these typeclases removes a large number of specialized `units R` lemmas as the lemmas about `R` now match themselves. A surprising number of lemmas elsewhere in the library can also be removed. The removed lemmas are: * Lemmas about `units` (replaced by `units.has_distrib_neg`): * `units.neg_one_pow_eq_or` * `units.neg_pow` * `units.neg_pow_bit0` * `units.neg_pow_bit1` * `units.neg_sq` * `units.neg_inv` (now `inv_neg'` for arbitrary groups with distributive negation) * `units.neg_neg` * `units.neg_mul` * `units.mul_neg` * `units.neg_mul_eq_neg_mul` * `units.neg_mul_eq_mul_neg` * `units.neg_mul_neg` * `units.neg_eq_neg_one_mul` * `units.mul_neg_one` * `units.neg_one_mul` * `semiconj_by.units_neg_right` * `semiconj_by.units_neg_right_iff` * `semiconj_by.units_neg_left` * `semiconj_by.units_neg_left_iff` * `semiconj_by.units_neg_one_right` * `semiconj_by.units_neg_one_left` * `commute.units_neg_right` * `commute.units_neg_right_iff` * `commute.units_neg_left` * `commute.units_neg_left_iff` * `commute.units_neg_one_right` * `commute.units_neg_one_left` * Lemmas about groups with zero (replaced by `group_with_zero.to_has_involutive_neg`): * `inv_inv₀` * `inv_involutive₀` * `inv_injective₀` * `inv_eq_iff` (now shared with the `inv_eq_iff_inv_eq` group lemma) * `eq_inv_iff` (now shared with the `eq_inv_iff_eq_inv` group lemma) * `equiv.inv₀` * `measurable_equiv.inv₀` * Lemmas about `ereal` (replaced by `ereal.has_involutive_neg`): * `ereal.neg_neg` * `ereal.neg_inj` * `ereal.neg_eq_neg_iff` * `ereal.neg_eq_iff_neg_eq` * Lemmas about `ennreal` (replaced by `ennreal.has_involutive_inv`): * `ereal.inv_inv` * `ereal.inv_involutive` * `ereal.inv_bijective` * `ereal.inv_eq_inv` * Other lemmas: * `ray_vector.neg_neg` * `module.ray.neg_neg` * `module.ray.neg_involutive` * `module.ray.eq_neg_iff_eq_neg` * `set.inv_inv` * `set.neg_neg` * `submonoid.inv_inv` * `add_submonoid.neg_neg` As a bonus, this provides the group `unitary R` with a negation operator and all the lemmas listed for `units` above. For now this doesn't attempt to unify `units.neg_smul` and `neg_smul`.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The new typeclasses are:
has_involutive_inv R, stating that(r⁻¹)⁻¹ = r(instances:
group,group_with_zero,ennreal,set,submonoid)has_involutive_neg R, stating that- -r = r(instances:
add_group,ereal,module.ray,ray_vector,set,add_submonoid,jordan_decomposition)has_distrib_neg R, stating that-a * b = a * -b = -(a * b)(instances:
ring,units,unitary,special_linear_group,GL_pos)While the original motivation only concerned the two
negtypeclasses, theto_additivemachinery forced the introduction ofhas_involutive_inv, which turned out to be used in more places than expected.Adding these typeclases removes a large number of specialized
units Rlemmas as the lemmas aboutRnow match themselves. A surprising number of lemmas elsewhere in the library can also be removed. The removed lemmas are:units(replaced byunits.has_distrib_neg):units.neg_one_pow_eq_orunits.neg_powunits.neg_pow_bit0units.neg_pow_bit1units.neg_squnits.neg_inv(nowinv_neg'for arbitrary groups with distributive negation)units.neg_negunits.neg_mulunits.mul_negunits.neg_mul_eq_neg_mulunits.neg_mul_eq_mul_negunits.neg_mul_negunits.neg_eq_neg_one_mulunits.mul_neg_oneunits.neg_one_mulsemiconj_by.units_neg_rightsemiconj_by.units_neg_right_iffsemiconj_by.units_neg_leftsemiconj_by.units_neg_left_iffsemiconj_by.units_neg_one_rightsemiconj_by.units_neg_one_leftcommute.units_neg_rightcommute.units_neg_right_iffcommute.units_neg_leftcommute.units_neg_left_iffcommute.units_neg_one_rightcommute.units_neg_one_leftgroup_with_zero.to_has_involutive_neg):inv_inv₀inv_involutive₀inv_injective₀inv_eq_iff(now shared with theinv_eq_iff_inv_eqgroup lemma)eq_inv_iff(now shared with theeq_inv_iff_eq_invgroup lemma)equiv.inv₀measurable_equiv.inv₀ereal(replaced byereal.has_involutive_neg):ereal.neg_negereal.neg_injereal.neg_eq_neg_iffereal.neg_eq_iff_neg_eqennreal(replaced byennreal.has_involutive_inv):ereal.inv_invereal.inv_involutiveereal.inv_bijectiveereal.inv_eq_invray_vector.neg_negmodule.ray.neg_negmodule.ray.neg_involutivemodule.ray.eq_neg_iff_eq_negset.inv_invset.neg_negsubmonoid.inv_invadd_submonoid.neg_negAs a bonus, this provides the group
unitary Rwith a negation operator and all the lemmas listed forunitsabove.For now this doesn't attempt to unify
units.neg_smulandneg_smul.