[Merged by Bors] - feat: Iic 2 = {0, 1, 2}#37557
Closed
vihdzp wants to merge 4 commits intoleanprover-community:masterfrom
Closed
[Merged by Bors] - feat: Iic 2 = {0, 1, 2}#37557vihdzp wants to merge 4 commits intoleanprover-community:masterfrom
Iic 2 = {0, 1, 2}#37557vihdzp wants to merge 4 commits intoleanprover-community:masterfrom
Conversation
Collaborator
vihdzp
commented
Apr 2, 2026
vihdzp
commented
PR summary 1a79483f50
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Algebra.Order.Monoid.Canonical.Defs | 194 | 195 | +1 (+0.52%) |
Import changes for all files
| Files | Import difference |
|---|---|
102 filesMathlib.Algebra.ContinuedFractions.Computation.Basic Mathlib.Algebra.Group.PNatPowAssoc Mathlib.Algebra.Order.AbsoluteValue.Basic Mathlib.Algebra.Order.AbsoluteValue.Euclidean Mathlib.Algebra.Order.AddGroupWithTop Mathlib.Algebra.Order.Algebra Mathlib.Algebra.Order.BigOperators.Group.List Mathlib.Algebra.Order.BigOperators.Group.Multiset Mathlib.Algebra.Order.BigOperators.Ring.List Mathlib.Algebra.Order.BigOperators.Ring.Multiset Mathlib.Algebra.Order.Field.Canonical Mathlib.Algebra.Order.Field.Power Mathlib.Algebra.Order.Floor.Defs Mathlib.Algebra.Order.Group.Nat Mathlib.Algebra.Order.GroupWithZero.Canonical Mathlib.Algebra.Order.GroupWithZero.Lex Mathlib.Algebra.Order.GroupWithZero.WithZero Mathlib.Algebra.Order.Hom.MonoidWithZero Mathlib.Algebra.Order.Hom.Ring Mathlib.Algebra.Order.Invertible Mathlib.Algebra.Order.Kleene Mathlib.Algebra.Order.Module.Algebra Mathlib.Algebra.Order.Module.Field Mathlib.Algebra.Order.Monoid.Associated Mathlib.Algebra.Order.Monoid.Canonical.Defs Mathlib.Algebra.Order.Monoid.Prod Mathlib.Algebra.Order.Monoid.ToMulBot Mathlib.Algebra.Order.Monoid.TypeTags Mathlib.Algebra.Order.Monoid.WithTop Mathlib.Algebra.Order.Nonneg.Floor Mathlib.Algebra.Order.PUnit Mathlib.Algebra.Order.Pi Mathlib.Algebra.Order.Ring.Abs Mathlib.Algebra.Order.Ring.Canonical Mathlib.Algebra.Order.Ring.Cast Mathlib.Algebra.Order.Ring.Nat Mathlib.Algebra.Order.Ring.Pow Mathlib.Algebra.Order.Ring.Prod Mathlib.Algebra.Order.Ring.WithTop Mathlib.Algebra.Order.Sub.Basic Mathlib.Algebra.Order.WithTop.Untop0 Mathlib.Algebra.Ring.BooleanRing Mathlib.Algebra.Ring.Identities Mathlib.Algebra.Ring.Subring.Order Mathlib.Algebra.Tropical.Basic Mathlib.Combinatorics.Quiver.Path.Decomposition Mathlib.Combinatorics.Quiver.Path.Vertices Mathlib.Control.Fix Mathlib.Data.Bool.Count Mathlib.Data.Int.AbsoluteValue Mathlib.Data.Int.Order.Lemmas Mathlib.Data.Int.Order.Units Mathlib.Data.List.Iterate Mathlib.Data.Multiset.DershowitzManna Mathlib.Data.Multiset.OrderedMonoid Mathlib.Data.Nat.BitIndices Mathlib.Data.Nat.Cast.Order.Ring Mathlib.Data.Nat.Dist Mathlib.Data.Nat.Upto Mathlib.Data.Num.Lemmas Mathlib.Data.Num.Prime Mathlib.Data.Num.ZNum Mathlib.Data.Ordmap.Invariants Mathlib.Data.Ordmap.Ordset Mathlib.Data.PNat.Basic Mathlib.Data.PNat.Factors Mathlib.Data.PNat.Find Mathlib.Data.PNat.Prime Mathlib.Data.PNat.Xgcd Mathlib.Data.Rat.Sqrt Mathlib.Data.String.Basic Mathlib.RingTheory.Coprime.Basic Mathlib.SetTheory.Lists Mathlib.Tactic.Bound Mathlib.Tactic.CancelDenoms Mathlib.Tactic.FieldSimp.Discharger Mathlib.Tactic.FieldSimp Mathlib.Tactic.Field Mathlib.Tactic.Finiteness Mathlib.Tactic.Group Mathlib.Tactic.Linarith.Datatypes Mathlib.Tactic.Linarith.Frontend Mathlib.Tactic.Linarith.Lemmas Mathlib.Tactic.Linarith.Oracle.FourierMotzkin Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm Mathlib.Tactic.Linarith.Parsing Mathlib.Tactic.Linarith.Preprocessing Mathlib.Tactic.Linarith.Verification Mathlib.Tactic.LinearCombination' Mathlib.Tactic.LinearCombination Mathlib.Tactic.NormNum.Abs Mathlib.Tactic.NormNum.DivMod Mathlib.Tactic.NormNum.Ineq Mathlib.Tactic.NormNum.ModEq Mathlib.Tactic.PNatToNat Mathlib.Tactic.Positivity.Basic Mathlib.Tactic.Positivity.Core Mathlib.Tactic.Positivity Mathlib.Tactic.Qify Mathlib.Tactic.Ring.Compare Mathlib.Tactic.Ring.PNat Mathlib.Tactic.Ring |
1 |
Declarations diff
+ Iic_one
+ Iic_two
+ Iio_one
+ Iio_two
+ isEmpty_Iio_one
- instIsEmptyIioZero
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).
artie2000
approved these changes
Apr 4, 2026
Contributor
|
Pull request successfully merged into master. Build succeeded:
|
mathlib-bors
bot
changed the title
Iic 2 = {0, 1, 2}Iic 2 = {0, 1, 2}
riccardobrasca
pushed a commit
to riccardobrasca/mathlib4
that referenced
this pull request
Apr 6, 2026
YellPika
pushed a commit
to YellPika/mathlib4
that referenced
this pull request
Apr 6, 2026
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
3 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.