[Merged by Bors] - feat(Logic/Basic): forall_and_index#27737
[Merged by Bors] - feat(Logic/Basic): forall_and_index#27737ChrisHughes24 wants to merge 8 commits intoleanprover-community:masterfrom
Conversation
PR summary c776b599a9Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
grunweg
left a comment
There was a problem hiding this comment.
Thanks!
maintainer delegate
|
🚀 Pull request has been placed on the maintainer queue by grunweg. |
|
Can you also add a backwards version |
I'm not sure about this. It would be very rarely used in the other direction, and more lemmas isn't always a good thing. |
|
-awaiting-author |
I asked for this because we have both Finset.sum_product and Finset.sum_product', and we also have Finset.sum_product_right and Finset.sum_product_right', so to me this looks like it's doing the same thing but with forall instead of sum and and instead of product. So if it was a good idea for the finset sums I think it should also be a good idea for the foralls. |
|
I counted the uses of import Mathlib
/-
MultilinearMap.domCoprod_alternization._simp_1_5
MonoidAlgebra.mul_apply_mul_eq_mul_of_uniqueMul._simp_1_1
AlgebraicTopology.AlternatingFaceMapComplex.d_squared._simp_1_1
Finset.expect_product'
PowerBasis.repr_mul_isIntegral
Finset.sum_smul_sum_eq_sum_perm
ArithmeticFunction.IsMultiplicative.mul
Matrix.induction_on'
Choose.choose_modEq_choose_mod_mul_choose_div
Fintype.sum_prod_type'
QuadraticMap.toQuadraticMap_toBilin._simp_1_1
Matrix.det_fromBlocks_zero₂₁._simp_1_1
Matrix.frobenius_nnnorm_diagonal._simp_1_1
-/
#eval do
let env ← Lean.getEnv
for i in env.constants do
if i.2.isUnsafe then continue
let some val := i.2.value? | continue
if val.containsConst (· == ``Finset.sum_product') then
Lean.logInfo (Lean.MessageData.ofConstName i.1)so it's at least seeing some use in mathlib. |
I've added the other version |
|
Thanks! bors merge |
|
bors r- |
|
Canceled. |
|
I'm not sure quite what went wrong when I hit merge. Can you merge master and make sure it builds? bors d+ |
|
✌️ ChrisHughes24 can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors d- |
|
I'm undelegating this, because one of the tests broke, so it should probably be checked again by somebody who understood what that test is for. |
|
-delegated |
|
cc @JovanGerb |
|
Oh, don't worry about that test too much. The test simply looks for all lemmas of a certain shape, and your new lemma now matches that shape, so it needs to be added. |
|
Though I'm having trouble understanding what is "left" about |
|
Maybe it can be called Also I think this should be labelled |
|
bors r+ |
|
Build failed: |
|
Failure looks like a temporary network issue? |
|
Pull request successfully merged into master. Build succeeded: |
* origin/master: (508 commits) feat(Logic/Basic): forall_and_index (leanprover-community#27737) feat(Algebra/intNorm): `x` divides `intNorm x` (leanprover-community#28021) feat(RingTheory/MvPolynomial/MonomialOrder): some lemmas about degree (leanprover-community#26000) chore: more elementary Motzkin polynomial proof (leanprover-community#28482) feat: e-seminormed monoid (leanprover-community#27385) feat(RingTheory): ` (⊥ : Ideal R) ^ n = ⊥` (leanprover-community#28171) fix(LinearAlgebra/Dimension/ErdosKaplansky): authorship (leanprover-community#28513) chore: golf entire `X_pow_eq_monomial` (leanprover-community#28504) feat(RingTheory): invertible modules and Picard group (leanprover-community#25337) chore: use delta `deriving` for leanprover-community#380 (leanprover-community#28498) feat: add bilinear maps for vector/matrix products (leanprover-community#28130) feat(Counterexamples): topologists' sine curve (leanprover-community#25833) feat(Analysis/Convex): doubly stochastic matrices have operator norm at most one (leanprover-community#28453) chore(Topology/Compactification): deprecate duplicate `ultrafilter_pure_injective` (leanprover-community#28436) feat: add `@[simp]` to `Multiset.cons_le_cons` and `Finset.insert_subset_insert` (leanprover-community#28285) feat: make `ring` work for semifields (leanprover-community#28494) feat: filtering lists and bounded quantifiers are primitive recursive (leanprover-community#26295) chore(Analysis/Analytic): split `Analytic.Basic` (leanprover-community#26270) refactor: tidy `mulVec` and `vecMul` lemmas about `•` (leanprover-community#28450) feat(Order/WellFounded): Acc and infinite descending chain (leanprover-community#28120) feat(NumberTheory/Padics): {Int,Rat}.padicValuation (leanprover-community#27667) chore(*): address a few timeout-related porting notes (leanprover-community#28483) feat(Algebra): toAlgebra_algebraMap (leanprover-community#28238) feat(Shrink): `IsCancelMul` instance (leanprover-community#28407) chore(Geometry): golf entire `chart_eq'` and `orthogonalProjection_orthogonalProjection` (leanprover-community#28485) feat: shifted geometric series and a `ProbabilityMeasure` version of `measure_iUnion_le` (leanprover-community#28087) chore(LinearAlgebra/PiTensorProduct): `rw` away use of `erw` in `lifts_zero` (leanprover-community#27554) feat(RingTheory): faithfully flat ring maps (leanprover-community#24530) chore(Geometry/RingedSpace): remove use of `erw` in `stalkSpecializes_stalkMap` (leanprover-community#27656) chore: add the Brownian motion project to downstream_repos.yml (leanprover-community#28459) feat(CategoryTheory/Sites/SheafOfTypes): composition of a sheaf with uliftFunctor is still a sheaf (leanprover-community#27816) feat(Valuation/DiscreteValuationRel): val relations with compatible valuations to Zm0 are IsDiscrete (leanprover-community#27213) chore(*): process a bunch of `aesop`-related porting notes (leanprover-community#28402) feat(CategoryTheory): abstract argument for the stability under transfinite compositions (leanprover-community#26030) chore: bump toolchain to v4.23.0-rc2 (leanprover-community#28454) chore(FieldTheory/Finite): fermat's little theorem in Nat form (leanprover-community#27962) feat(Combinatorics/SimpleGraph/Paths): add theorem `SimpleGraph.Walk.IsPath.concat` (leanprover-community#27582) feat(Slope): slope_pos_iff_of_le and related lemmas (leanprover-community#28039) feat: tactic analysis framework (leanprover-community#26683) chore(Data/EReal): deprecate `add_pos_of_nonneg_of_pos` and `add_ne_top_iff_of_ne_bot` (duplicates) (leanprover-community#28424) feat(MathlibTest/FieldSimp): add a few more tests (leanprover-community#28413) chore(RingTheory/HahnSeries): deprecate duplicate `orderTop_add_orderTop_le_orderTop_mul` (leanprover-community#28231) chore(AlgebraicGeometry/IdealSheaf): deprecate duplicate `AlgebraicGeometry.Scheme.IdealSheafData.Scheme.zeroLocus_radical` (leanprover-community#28202) feat(Algebra/Order): ArchimedeanClass ball (leanprover-community#27885) chore(Geometry/RingedSpace): remove use of `erw` in `isUnit_of_isUnit_germ` (leanprover-community#27660) feat(SkewMonoidAlgebra): coeff_mul lemmas (leanprover-community#27255) chore(LinearAlgebra): golf entire `isUnit_det` (leanprover-community#28438) chore(FieldTheory/IntermediateField): golf entire `coe_sum` and `coe_prod` (leanprover-community#28431) feat: separate linter error message for empty doc-strings (leanprover-community#27895) feat(RingTheory/PowerSeries/Binomial): add basic lemmas, golf (leanprover-community#27497) ...
A generalization of
and_imp. It may cause a linter error because of thesimpattribute. I wasn't that sure about the name.