chore(Data/Int/Init): generalize le_induction from Prop to Sort* + def lemmas#37171
Open
SnirBroshi wants to merge 5 commits intoleanprover-community:masterfrom
Open
chore(Data/Int/Init): generalize le_induction from Prop to Sort* + def lemmas#37171SnirBroshi wants to merge 5 commits intoleanprover-community:masterfrom
le_induction from Prop to Sort* + def lemmas#37171SnirBroshi wants to merge 5 commits intoleanprover-community:masterfrom
Conversation
PR summary 93349c600fImport changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Data.Int.Init | 55 | 57 | +2 (+3.64%) |
| Mathlib.Data.Int.Basic | 109 | 111 | +2 (+1.83%) |
Import changes for all files
| Files | Import difference |
|---|---|
249 filesMathlib.Algebra.EuclideanDomain.Field Mathlib.Algebra.EuclideanDomain.Int Mathlib.Algebra.Field.Basic Mathlib.Algebra.Field.MinimalAxioms Mathlib.Algebra.Field.ModEq Mathlib.Algebra.Field.ULift Mathlib.Algebra.Free Mathlib.Algebra.Group.Action.Basic Mathlib.Algebra.Group.Action.Hom Mathlib.Algebra.Group.Action.Opposite Mathlib.Algebra.Group.Action.Pointwise.Set.Basic Mathlib.Algebra.Group.Action.Pretransitive Mathlib.Algebra.Group.Action.Prod Mathlib.Algebra.Group.Action.TypeTags Mathlib.Algebra.Group.Action.Units Mathlib.Algebra.Group.Basic Mathlib.Algebra.Group.Center Mathlib.Algebra.Group.Commute.Basic Mathlib.Algebra.Group.Commute.Units Mathlib.Algebra.Group.Equiv.Basic Mathlib.Algebra.Group.Equiv.Opposite Mathlib.Algebra.Group.Equiv.TypeTags Mathlib.Algebra.Group.Even Mathlib.Algebra.Group.Hom.Basic Mathlib.Algebra.Group.Hom.End Mathlib.Algebra.Group.Hom.Instances Mathlib.Algebra.Group.Idempotent Mathlib.Algebra.Group.Indicator Mathlib.Algebra.Group.Int.TypeTags Mathlib.Algebra.Group.Int.Units Mathlib.Algebra.Group.Invertible.Basic Mathlib.Algebra.Group.Irreducible.Lemmas Mathlib.Algebra.Group.ModEq Mathlib.Algebra.Group.Nat.Even Mathlib.Algebra.Group.Nat.Hom Mathlib.Algebra.Group.Nat.TypeTags Mathlib.Algebra.Group.Opposite Mathlib.Algebra.Group.Pi.Lemmas Mathlib.Algebra.Group.Pointwise.Set.Basic Mathlib.Algebra.Group.Pointwise.Set.Lattice Mathlib.Algebra.Group.Pointwise.Set.Small Mathlib.Algebra.Group.Prod Mathlib.Algebra.Group.Semiconj.Basic Mathlib.Algebra.Group.Semiconj.Units Mathlib.Algebra.Group.Submonoid.DistribMulAction Mathlib.Algebra.Group.Submonoid.MulOpposite Mathlib.Algebra.Group.Submonoid.Operations Mathlib.Algebra.Group.Subsemigroup.Operations Mathlib.Algebra.Group.Support Mathlib.Algebra.Group.Torsion Mathlib.Algebra.Group.TypeTags.Basic Mathlib.Algebra.Group.TypeTags.Hom Mathlib.Algebra.Group.TypeTags.Pointwise Mathlib.Algebra.Group.Units.Basic Mathlib.Algebra.Group.Units.Equiv Mathlib.Algebra.Group.Units.Hom Mathlib.Algebra.Group.Units.Opposite Mathlib.Algebra.GroupWithZero.Action.Defs Mathlib.Algebra.GroupWithZero.Action.End Mathlib.Algebra.GroupWithZero.Action.Hom Mathlib.Algebra.GroupWithZero.Action.Opposite Mathlib.Algebra.GroupWithZero.Action.Prod Mathlib.Algebra.GroupWithZero.Action.Units Mathlib.Algebra.GroupWithZero.Basic Mathlib.Algebra.GroupWithZero.Center Mathlib.Algebra.GroupWithZero.Commute Mathlib.Algebra.GroupWithZero.Equiv Mathlib.Algebra.GroupWithZero.Hom Mathlib.Algebra.GroupWithZero.Idempotent Mathlib.Algebra.GroupWithZero.Indicator Mathlib.Algebra.GroupWithZero.Invertible Mathlib.Algebra.GroupWithZero.Opposite Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic Mathlib.Algebra.GroupWithZero.Semiconj Mathlib.Algebra.GroupWithZero.Submonoid.Instances Mathlib.Algebra.GroupWithZero.Units.Basic Mathlib.Algebra.GroupWithZero.Units.Equiv Mathlib.Algebra.GroupWithZero.Units.Lemmas Mathlib.Algebra.Homology.Embedding.Basic Mathlib.Algebra.Module.Defs Mathlib.Algebra.Module.MinimalAxioms Mathlib.Algebra.Module.Opposite Mathlib.Algebra.Module.PUnit Mathlib.Algebra.Module.PointwisePi Mathlib.Algebra.Module.Prod Mathlib.Algebra.Module.RingHom Mathlib.Algebra.Order.AddGroupWithTop Mathlib.Algebra.Order.AddTorsor Mathlib.Algebra.Order.BigOperators.GroupWithZero.List Mathlib.Algebra.Order.Field.Pointwise Mathlib.Algebra.Order.Group.Abs Mathlib.Algebra.Order.Group.Action.Flag Mathlib.Algebra.Order.Group.Action Mathlib.Algebra.Order.Group.Basic Mathlib.Algebra.Order.Group.Bounds Mathlib.Algebra.Order.Group.CompleteLattice Mathlib.Algebra.Order.Group.Defs Mathlib.Algebra.Order.Group.DenselyOrdered Mathlib.Algebra.Order.Group.Indicator Mathlib.Algebra.Order.Group.Int Mathlib.Algebra.Order.Group.Lattice Mathlib.Algebra.Order.Group.MinMax Mathlib.Algebra.Order.Group.Nat Mathlib.Algebra.Order.Group.Opposite Mathlib.Algebra.Order.Group.OrderIso Mathlib.Algebra.Order.Group.Pointwise.Bounds Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice Mathlib.Algebra.Order.Group.PosPart Mathlib.Algebra.Order.Group.Unbundled.Abs Mathlib.Algebra.Order.Group.Unbundled.Basic Mathlib.Algebra.Order.Group.Unbundled.Int Mathlib.Algebra.Order.Group.Units Mathlib.Algebra.Order.GroupWithZero.Bounds Mathlib.Algebra.Order.GroupWithZero.Submonoid Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso Mathlib.Algebra.Order.Hom.Basic Mathlib.Algebra.Order.Hom.Monoid Mathlib.Algebra.Order.Hom.Submonoid Mathlib.Algebra.Order.Hom.TypeTags Mathlib.Algebra.Order.Hom.Units Mathlib.Algebra.Order.Interval.Set.Group Mathlib.Algebra.Order.Interval.Set.Instances Mathlib.Algebra.Order.Interval.Set.Monoid Mathlib.Algebra.Order.Monoid.Basic Mathlib.Algebra.Order.Monoid.Canonical.Defs Mathlib.Algebra.Order.Monoid.Defs Mathlib.Algebra.Order.Monoid.Lex Mathlib.Algebra.Order.Monoid.NatCast Mathlib.Algebra.Order.Monoid.OrderDual Mathlib.Algebra.Order.Monoid.Prod Mathlib.Algebra.Order.Monoid.Submonoid Mathlib.Algebra.Order.Monoid.TypeTags Mathlib.Algebra.Order.Monoid.Unbundled.Basic Mathlib.Algebra.Order.Monoid.Unbundled.Defs Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE Mathlib.Algebra.Order.Monoid.Unbundled.MinMax Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual Mathlib.Algebra.Order.Monoid.Unbundled.Pow Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags Mathlib.Algebra.Order.Monoid.Unbundled.Units Mathlib.Algebra.Order.Monoid.Unbundled.WithTop Mathlib.Algebra.Order.Monoid.WithTop Mathlib.Algebra.Order.PUnit Mathlib.Algebra.Order.Pi Mathlib.Algebra.Order.Positive.Field Mathlib.Algebra.Order.Positive.Ring Mathlib.Algebra.Order.Quantale Mathlib.Algebra.Order.Ring.Defs Mathlib.Algebra.Order.Ring.Idempotent Mathlib.Algebra.Order.Ring.InjSurj Mathlib.Algebra.Order.Ring.Opposite Mathlib.Algebra.Order.Ring.Unbundled.Basic Mathlib.Algebra.Order.Sub.Basic Mathlib.Algebra.Order.Sub.Defs Mathlib.Algebra.Order.Sub.Prod Mathlib.Algebra.Order.Sub.Unbundled.Basic Mathlib.Algebra.Order.Sub.Unbundled.Hom Mathlib.Algebra.Order.Sub.WithTop Mathlib.Algebra.Regular.Basic Mathlib.Algebra.Regular.Pi Mathlib.Algebra.Regular.Prod Mathlib.Algebra.Regular.SMul Mathlib.Algebra.Regular.ULift Mathlib.Algebra.Ring.Action.Basic Mathlib.Algebra.Ring.Action.Field Mathlib.Algebra.Ring.Action.Rat Mathlib.Algebra.Ring.Basic Mathlib.Algebra.Ring.Centralizer Mathlib.Algebra.Ring.Commute Mathlib.Algebra.Ring.CompTypeclasses Mathlib.Algebra.Ring.Equiv Mathlib.Algebra.Ring.GrindInstances Mathlib.Algebra.Ring.Hom.Defs Mathlib.Algebra.Ring.Hom.InjSurj Mathlib.Algebra.Ring.Idempotent Mathlib.Algebra.Ring.InjSurj Mathlib.Algebra.Ring.Int.Defs Mathlib.Algebra.Ring.Int.Units Mathlib.Algebra.Ring.Invertible Mathlib.Algebra.Ring.MinimalAxioms Mathlib.Algebra.Ring.Opposite Mathlib.Algebra.Ring.Pi Mathlib.Algebra.Ring.Pointwise.Set Mathlib.Algebra.Ring.Regular Mathlib.Algebra.Ring.Subsemiring.Defs Mathlib.Algebra.Ring.Subsemiring.Order Mathlib.Algebra.Ring.Torsion Mathlib.Algebra.Ring.ULift Mathlib.Algebra.Ring.Units Mathlib.Algebra.Tropical.Basic Mathlib.Algebra.Tropical.Lattice Mathlib.Combinatorics.Quiver.Path.Decomposition Mathlib.Combinatorics.Quiver.Path.Weight Mathlib.Control.Fix Mathlib.Data.FP.Basic Mathlib.Data.Int.Basic Mathlib.Data.Int.Cast.Basic Mathlib.Data.Int.Cast.Field Mathlib.Data.Int.Cast.Prod Mathlib.Data.Int.ConditionallyCompleteOrder Mathlib.Data.Int.Init Mathlib.Data.Int.LeastGreatest Mathlib.Data.Int.NatAbs Mathlib.Data.Int.Range Mathlib.Data.List.Iterate Mathlib.Data.Nat.Cast.Commute Mathlib.Data.Nat.Cast.Prod Mathlib.Data.Nat.Cast.WithTop Mathlib.Data.Nat.PSub Mathlib.Data.Nat.Upto Mathlib.Data.Nat.WithBot Mathlib.Data.Ordmap.Ordnode Mathlib.GroupTheory.Congruence.Basic Mathlib.GroupTheory.GroupAction.DomAct.ActionHom Mathlib.GroupTheory.GroupAction.DomAct.Basic Mathlib.GroupTheory.GroupAction.Embedding Mathlib.GroupTheory.GroupAction.Hom Mathlib.GroupTheory.GroupAction.Pointwise Mathlib.GroupTheory.GroupAction.Ring Mathlib.GroupTheory.GroupAction.Support Mathlib.GroupTheory.Submonoid.Center Mathlib.GroupTheory.Submonoid.Centralizer Mathlib.GroupTheory.Subsemigroup.Center Mathlib.GroupTheory.Subsemigroup.Centralizer Mathlib.Order.CompleteLattice.Group Mathlib.Order.ConditionallyCompleteLattice.Group Mathlib.Order.Filter.AtTopBot.Field Mathlib.Order.Filter.AtTopBot.Group Mathlib.Order.Filter.AtTopBot.Monoid Mathlib.Order.Filter.AtTopBot.Ring Mathlib.Order.Monotone.Odd Mathlib.Order.SemiconjSup Mathlib.RingTheory.Congruence.Basic Mathlib.RingTheory.Congruence.Defs Mathlib.RingTheory.Congruence.Opposite Mathlib.RingTheory.NonUnitalSubsemiring.Defs Mathlib.RingTheory.OreLocalization.OreSet Mathlib.RingTheory.RingInvo Mathlib.SetTheory.Lists Mathlib.Tactic.CancelDenoms.Core Mathlib.Tactic.Monotonicity.Lemmas Mathlib.Tactic.Monotonicity Mathlib.Tactic.MoveAdd Mathlib.Tactic.NormNum.Core Mathlib.Tactic.NormNum.Parity Mathlib.Tactic.NormNum.Result Mathlib.Tactic.Zify |
2 |
Declarations diff
+ leInduction
+ leInductionDown
+ leInductionDown_base
+ leInductionDown_sub_one
+ leInduction_add_one
+ leInduction_base
You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/reporting/technical-debt-metrics.sh 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).
Contributor
|
Can you uniquely characterize the new definitions with some defining lemmas? |
Collaborator
Author
|
What do you mean? |
Contributor
|
I mean iota reduction lemmas like
We definitely want API for each and every definition that's going into mathlib. |
SnirBroshi
changed the title
le_induction from Prop to Sort*le_induction from Prop to Sort* + def lemmas
github-actions
bot
added
the
large-import
mathlib-merge-conflicts
bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
github-actions
bot
removed
the
merge-conflict
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
Zulip 💬