[Merged by Bors] - feat(Algebra/Group/Pointwise/Set): add IsSelfInv predicate - #42611
justus-springer wants to merge 31 commits into
Conversation
PR summary d8bed3ea36
|
| Files | Import difference |
|---|---|
| ../mathlib-ci/scripts/pr_summary/import_trans_difference.sh all | |
| There are 6737 files with changed transitive imports taking up over 304068 characters: this is too many to display! | |
You can run this locally from your mathlib4 directory: |
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
Declarations diff (regex)
+ IsOfFinOrder.isSelfInv_iff
+ IsSelfInv
+ IsSelfInv.compl
+ IsSelfInv.conj
+ IsSelfInv.diff
+ IsSelfInv.div
+ IsSelfInv.empty
+ IsSelfInv.eq_inv
+ IsSelfInv.iInter
+ IsSelfInv.iUnion
+ IsSelfInv.inter
+ IsSelfInv.inv
+ IsSelfInv.inv_eq
+ IsSelfInv.inv_mem
+ IsSelfInv.inv_subset
+ IsSelfInv.mul
+ IsSelfInv.neg
+ IsSelfInv.of_compl
+ IsSelfInv.of_invMemClass
+ IsSelfInv.of_inv_eq
+ IsSelfInv.of_inv_subset
+ IsSelfInv.of_subset_inv
+ IsSelfInv.one
+ IsSelfInv.pow
+ IsSelfInv.prod
+ IsSelfInv.sInter
+ IsSelfInv.sUnion
+ IsSelfInv.subset_inv
+ IsSelfInv.union
+ IsSelfInv.univ
+ IsSelfInv.zero
+ IsSelfInv.zpow
+ IsSelfNeg.inv
+ IsSelfNeg.one
+ Pi.isSelfInv_iff
+ instance [DecidableEq α] : Decidable (IsSelfInv a) := decidable_of_iff _ isSelfInv_iff.symm
+ isSelfInv_compl_iff
+ isSelfInv_conj_iff
+ isSelfInv_iff_eq_neg_one_or_eq_zero_or_eq_one
+ isSelfInv_iff_eq_one
+ isSelfInv_iff_forall_inv_mem
+ isSelfInv_iff_forall_inv_mem_iff
+ isSelfInv_iff_inv_subset
+ isSelfInv_iff_isOfFinOrder_and_orderOf_le_two
+ isSelfInv_iff_sq_eq_one
+ isSelfInv_iff_subset_inv
+ isSelfInv_inv
+ isSelfInv_neg_iff
+ isSelfInv_singleton_iff
+ isSelfNeg_inv_iff
+ isSelfNeg_of_isSMulRegular_two
++ isSelfInv_iff
You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.
Declarations diff (Lean)
✅ Lean-aware diff — post-build, computed from the Lean environment (commit
d8bed3e).
- +98 new declarations
- −0 removed declarations
+IsOfFinAddOrder.isSelfNeg_iff
+IsOfFinOrder.isSelfInv_iff
+IsSelfInv
+IsSelfInv.compl
+IsSelfInv.conj
+IsSelfInv.diff
+IsSelfInv.div
+IsSelfInv.empty
+IsSelfInv.eq_inv
+IsSelfInv.iInter
+IsSelfInv.iUnion
+IsSelfInv.inter
+IsSelfInv.inv
+IsSelfInv.inv_eq
+IsSelfInv.inv_mem
+IsSelfInv.inv_subset
+IsSelfInv.mul
+IsSelfInv.neg
+IsSelfInv.of_compl
+IsSelfInv.of_invMemClass
+IsSelfInv.of_inv_eq
+IsSelfInv.of_inv_subset
+IsSelfInv.of_subset_inv
+IsSelfInv.one
+IsSelfInv.pow
+IsSelfInv.prod
+IsSelfInv.sInter
+IsSelfInv.sUnion
+IsSelfInv.subset_inv
+IsSelfInv.union
+IsSelfInv.univ
+IsSelfInv.zero
+IsSelfInv.zpow
+IsSelfNeg
+IsSelfNeg.add
+IsSelfNeg.addConj
+IsSelfNeg.compl
+IsSelfNeg.diff
+IsSelfNeg.empty
+IsSelfNeg.eq_neg
+IsSelfNeg.iInter
+IsSelfNeg.iUnion
+IsSelfNeg.inter
+IsSelfNeg.inv
+IsSelfNeg.neg
+IsSelfNeg.neg_eq
+IsSelfNeg.neg_mem
+IsSelfNeg.neg_subset
+IsSelfNeg.nsmul
+IsSelfNeg.of_compl
+IsSelfNeg.of_negMemClass
+IsSelfNeg.of_neg_eq
+IsSelfNeg.of_neg_subset
+IsSelfNeg.of_subset_neg
+IsSelfNeg.one
+IsSelfNeg.sInter
+IsSelfNeg.sUnion
+IsSelfNeg.sub
+IsSelfNeg.subset_neg
+IsSelfNeg.sum
+IsSelfNeg.union
+IsSelfNeg.univ
+IsSelfNeg.zero
+IsSelfNeg.zsmul
+Pi.isSelfInv_iff
+Pi.isSelfNeg_iff
+Prod.isSelfInv_iff
+Prod.isSelfNeg_iff
+instDecidableIsSelfInvOfDecidableEq
+instDecidableIsSelfNegOfDecidableEq
+isSelfInv_compl_iff
+isSelfInv_conj_iff
+isSelfInv_iff
+isSelfInv_iff_eq_neg_one_or_eq_zero_or_eq_one
+isSelfInv_iff_eq_one
+isSelfInv_iff_forall_inv_mem
+isSelfInv_iff_forall_inv_mem_iff
+isSelfInv_iff_inv_subset
+isSelfInv_iff_isOfFinOrder_and_orderOf_le_two
+isSelfInv_iff_sq_eq_one
+isSelfInv_iff_subset_inv
+isSelfInv_inv
+isSelfInv_neg_iff
+isSelfInv_singleton_iff
+isSelfNeg_addConj_iff
+isSelfNeg_compl_iff
+isSelfNeg_iff
+isSelfNeg_iff_eq_zero
+isSelfNeg_iff_forall_neg_mem
+isSelfNeg_iff_forall_neg_mem_iff
+isSelfNeg_iff_isOfFinAddOrder_and_addOrderOf_le_two
+isSelfNeg_iff_neg_subset
+isSelfNeg_iff_subset_neg
+isSelfNeg_iff_two_nsmul_eq_zero
+isSelfNeg_inv_iff
+isSelfNeg_neg
+isSelfNeg_of_isSMulRegular_two
+isSelfNeg_singleton_iffNo changes to strong technical debt.
Increase in weak tech debt: (relative, absolute) = (1.00, 1.00)
| Current number | Change | Type (weak) |
|---|---|---|
| large files | 1 | 1 |
| exposed public sections | 5031 | 1 |
Current commit d8bed3ea36
Reference commit b7527c8e1d
This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
justus-springer
changed the title
IsMulSymmetric predicateIsInvClosed predicate
Co-authored-by: Aaron Liu <aaronliu2008@outlook.com>
Co-authored-by: Aaron Liu <aaronliu2008@outlook.com>
YaelDillies
left a comment
YaelDillies
left a comment
There was a problem hiding this comment.
Can you show closure under cartesian products and multiplication (assuming commutativity)?
YaelDillies
added
the
awaiting-author
justus-springer
added
t-algebra
YaelDillies
added
the
awaiting-author
justus-springer
added
awaiting-CI
justus-springer
added
awaiting-CI
github-actions
Bot
removed
the
awaiting-CI
|
The last commit after the maintainer merge moved two lemmas ( |
justus-springer
removed
the
large-import
j-loreaux
left a comment
j-loreaux
left a comment
There was a problem hiding this comment.
Looks nice. I do wish there were a way to unify this further with IsSelfAdjoint so that we get all the generic theorems for free, but I think it would probably be more trouble than it's worth at the moment.
bors +
|
Did you mean "r+"? |
|
oops bors d+ |
mathlib-bors
Bot
added
the
delegated
|
✌️ justus-springer can now approve this pull request until 2026-09-15 22:25 UTC (in 2 weeks). To approve and merge, reply with
|
mathlib-triage
Bot
removed
the
maintainer-merge
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
|
bors r+ |
See also #36605 for the discussion that led to this PR. We add a predicate for terms to be self-inverse in a type with inversion and add basic API. We apply this also to pointwise operations on sets. The lemma `InvMemClass.isSelfInv` relates this to the existing `InvMemClass`, which will make it easy to show that e.g. additive subgroups are closed under negation. Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
mathlib-bors
Bot
added
the
bors-staging
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
Bot
changed the title
IsSelfInv predicateIsSelfInv predicate
mathlib-bors
Bot
removed
the
delegated
…d negation (#36605) Prove lemmas about the interaction of hull, span and negation. Main additions: * `PointedCone.toSubmodule` that produces a submodule with the same support given that `IsSelfNeg C`. Also the corresponding `CanLift` * `PointedCone.hull_neg_pair_eq_span_singleton` proving `hull R {-x, x} = R ∙ x` (simp lemma) * `PointedCone.span_eq_hull_neg_sup_hull` proving `span R s = hull R (-s) ⊔ hull R s` * `PointedCone.mem_span` proving `x ∈ span R C ↔ ∃ p, n ∈ C, x = p - n` #### Note This PR resulted in #42611 and the introduction of `IsSelfNeg` to unify several ways to express the same fact: * `-C = C` * `-C ≤ C` or `C ≤ -C` * `C = span R C` * `C = C.lineal` Co-authored by: Olivia Röhrig, Kilian Rueß, Artie Khovanov Co-authored-by: Martin Winter <martin.winter.math@gmail.com>
…ver-community#42611) See also leanprover-community#36605 for the discussion that led to this PR. We add a predicate for terms to be self-inverse in a type with inversion and add basic API. We apply this also to pointwise operations on sets. The lemma `InvMemClass.isSelfInv` relates this to the existing `InvMemClass`, which will make it easy to show that e.g. additive subgroups are closed under negation. Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
…d negation (leanprover-community#36605) Prove lemmas about the interaction of hull, span and negation. Main additions: * `PointedCone.toSubmodule` that produces a submodule with the same support given that `IsSelfNeg C`. Also the corresponding `CanLift` * `PointedCone.hull_neg_pair_eq_span_singleton` proving `hull R {-x, x} = R ∙ x` (simp lemma) * `PointedCone.span_eq_hull_neg_sup_hull` proving `span R s = hull R (-s) ⊔ hull R s` * `PointedCone.mem_span` proving `x ∈ span R C ↔ ∃ p, n ∈ C, x = p - n` #### Note This PR resulted in leanprover-community#42611 and the introduction of `IsSelfNeg` to unify several ways to express the same fact: * `-C = C` * `-C ≤ C` or `C ≤ -C` * `C = span R C` * `C = C.lineal` Co-authored by: Olivia Röhrig, Kilian Rueß, Artie Khovanov Co-authored-by: Martin Winter <martin.winter.math@gmail.com>
|
|
||
| public section | ||
|
|
||
| open Set |
There was a problem hiding this comment.
I think I claim this should all be in the Set namespace.
There was a problem hiding this comment.
I agree for lemmas like isSelfInv_iff_forall_inv_mem_iff . But much of this file is putting lemmas into IsSelfInv namespace to make available for dot notation. I guess we could also put those into Set, e.g. Set.IsSelfInv.inter, using the "dot-notation-respects-open" feature. But it seems not everyone likes this feature.
There was a problem hiding this comment.
Opened #43792 (I put everything in the Set namespace for now).
| /-! | ||
| # Self-inverse elements | ||
|
|
||
| This file defines self-inverse elements of a type with an inversion, i.e. elements `a` satisfying | ||
| `a⁻¹ = a`. | ||
|
|
||
| ## Main declarations | ||
|
|
||
| * `IsSelfInv a`: The element `a` satisfies `a⁻¹ = a`. | ||
| * `IsSelfNeg a`: The element `a` satisfies `-a = a`. | ||
| -/ |
There was a problem hiding this comment.
Could you make a follow-up PR that extends the docstring to explain why this is useful? I believe that it is, but would prefer not to have to
- Find the commit message associated with defining these
- Follow the reference, "See also [Merged by Bors] - feat(Geometry/Convex/Cone): lemmas about interaction of hull, span and negation #36605 for the discussion that led to this PR."
- Work out which part of the discussion is the reason.
In order to understand why I should choose it over writing a = -a.
Is the answer as simple as "IsSelfInv (oneReally bigExpression) is nicer to read than oneReallyBig Expression = -oneReallyBig Expression"?
There was a problem hiding this comment.
Will do. The main point is just to have a canonical way of talking about self-inverse elements (or "symmetric sets"). That's how it showed up in the discussion of the cones PR. And indeed, we have places in the library where we write A⁻¹ = A for sets, and other places where it's ∀ x ∈ A, x⁻¹ ∈ A.
7 participants
See also #36605 for the discussion that led to this PR.
We add a predicate for terms to be self-inverse in a type with inversion and add basic API. We apply this also to pointwise operations on sets. The lemma
InvMemClass.isSelfInvrelates this to the existingInvMemClass, which will make it easy to show that e.g. additive subgroups are closed under negation.