Conversation
This reverts commit 751b341.
PR summary 9b846cfdc2Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.SetTheory.ZFC.Ordinal | 486 | 666 | +180 (+37.04%) |
| Mathlib.Order.SuccPred.CompleteLinearOrder | 377 | 378 | +1 (+0.27%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Order.SuccPred.CompleteLinearOrder |
1 |
Mathlib.SetTheory.ZFC.Ordinal |
180 |
Declarations diff
+ IsOrdinal.toZFSet_rank_eq
+ _root_.Ordinal.toZFSetIso
+ _root_.PSet.rank_mk
+ antisymm_iff
+ eq_of_subset_of_subset
+ iSup_succ
+ instance : HasSSubset PSet
+ instance : HasSSubset ZFSet
+ instance : PartialOrder ZFSet
+ instance : Preorder PSet
+ isOrdinal_iff_mem_range_toZFSet
+ isOrdinal_toZFSet
+ mem_def
+ mem_iff_rank_lt
+ mem_toPSet_iff
+ mem_toZFSet_iff
+ mk_toPSet
+ rank_inj
+ rank_toPSet
+ rank_toZFSet
+ subset_iff_rank_le
+ toPSet
+ toZFSet
+ toZFSet_mem_toZFSet_iff
+ toZFSet_subset_toZFSet_iff
+ toZFSet_toSet
+ type_toPSet
++ le_def
++ lt_def
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 script/declarations_diff.sh contains some details about this script.
Increase in tech debt: (relative, absolute) = (2.00, 0.02)
| Current number | Change | Type |
|---|---|---|
| 89 | 2 | disabled deprecation lints |
Current commit 9b846cfdc2
Reference commit ffcd1a0e57
You can run this locally as
./scripts/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).
|
This PR/issue depends on: |
|
Moved to #26544. |
We define `Ordinal.toZFSet` and prove that its outputs are precisely the ZFC ordinals. Moved from #19985.
We define
Ordinal.toZFSetand prove that its outputs are precisely the ZFC ordinals.⨆ a < x, succ a = x#19970