feat(Tactic): generalize ofScientific NormNum extension to `DivisionSemiring` by DavidLedvinka · Pull Request #34805 · leanprover-community/mathlib4

DavidLedvinka · 2026-02-03T20:34:48Z

Co-authored-by: @hrmacbeth

This reverts commit 00f4eb5.

github-actions · 2026-02-03T20:36:02Z

PR summary a499e40942

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ evalNNRatCast
+ evalNNRealDivNat
+ isNNRat_natDiv
+ isNNRat_nnratCast
+ isNat_nnratCast

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 relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

mathlib-merge-conflicts · 2026-02-18T06:15:05Z

This pull request has conflicts, please merge master and resolve them.

Mathlib/Tactic/NormNum/OfScientific.lean

Mathlib/Tactic/NormNum/Inv.lean

Co-authored-by: Jovan Gerbscheid <[email protected]>

…into ring_test

Co-authored-by: Jovan Gerbscheid <[email protected]>

DavidLedvinka · 2026-02-18T17:20:29Z

I added set_option backward.isDefEq.respectTransparency false in to fix a broken proof. I guess we should wait for the official announcement/decision about this (as suggested by @eric-wieser here) before merging or trying to fix it.

Mathlib/Tactic/NormNum/Inv.lean

Co-authored-by: Eric Wieser <[email protected]>

Mathlib/Tactic/NormNum/Inv.lean

mathlib-merge-conflicts · 2026-02-24T23:03:52Z

This pull request has conflicts, please merge master and resolve them.

DavidLedvinka · 2026-03-21T19:31:08Z

-awaiting-author

David Ledvinka added 9 commits January 24, 2026 23:53

test

00f4eb5

Revert "test"

6165595

This reverts commit 00f4eb5.

Merge branch 'master' of https://github.com/DavidLedvinka/mathlib4

38e69bf

Merge branch 'master' of https://github.com/DavidLedvinka/mathlib4

97b18e8

Merge branch 'master' of https://github.com/DavidLedvinka/mathlib4

72423dd

erge branch 'master' of https://github.com/DavidLedvinka/mathlib4

0ba4995

test

90349fa

remove accidental file

78f3844

finished rough copy

cd289c2

github-actions bot added the t-meta Tactics, attributes or user commands label Feb 3, 2026

David Ledvinka added 2 commits February 3, 2026 21:28

fix lint

6e75030

minor fix

9a9f59d

DavidLedvinka marked this pull request as ready for review February 3, 2026 22:24

mathlib-triage bot assigned alexjbest Feb 7, 2026

alexjbest removed their assignment Feb 7, 2026

mathlib-triage bot assigned JovanGerb Feb 11, 2026

mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 18, 2026

JovanGerb approved these changes Feb 18, 2026

View reviewed changes

DavidLedvinka and others added 8 commits February 18, 2026 14:26

Update Mathlib/Tactic/NormNum/OfScientific.lean

fe3492f

Co-authored-by: Jovan Gerbscheid <[email protected]>

Update Mathlib/Tactic/NormNum/Inv.lean

6a5b276

Co-authored-by: Jovan Gerbscheid <[email protected]>

Merge branch 'master' into ring_test

b296649

merge master

79c0238

Merge branch 'ring_test' of https://github.com/DavidLedvinka/mathlib4 …

5dd35d4

…into ring_test

Update Mathlib/Tactic/NormNum/OfScientific.lean

517bf52

Co-authored-by: Jovan Gerbscheid <[email protected]>

suggestions

b0b016d

Merge branch 'master' into ring_test

9570bcb

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 18, 2026

backward_isDefEq

2b61de0

eric-wieser reviewed Feb 18, 2026

View reviewed changes

Mathlib/Tactic/NormNum/Inv.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Feb 18, 2026

View reviewed changes

Mathlib/Tactic/NormNum/Inv.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Feb 18, 2026

View reviewed changes

Mathlib/Tactic/NormNum/Inv.lean Outdated Show resolved Hide resolved

DavidLedvinka and others added 5 commits February 18, 2026 18:10

Update Mathlib/Tactic/NormNum/Inv.lean

1197aa4

Co-authored-by: Eric Wieser <[email protected]>

Update Mathlib/Tactic/NormNum/Inv.lean

2628946

Co-authored-by: Eric Wieser <[email protected]>

clean up

f7cd021

test

58ee9a9

test

fc6837b

b-mehta reviewed Feb 24, 2026

View reviewed changes

Mathlib/Tactic/NormNum/Inv.lean Outdated Show resolved Hide resolved

Mathlib/Tactic/NormNum/Inv.lean Outdated Show resolved Hide resolved

b-mehta added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 24, 2026

mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 24, 2026

merge master

f32a922

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 21, 2026

David Ledvinka added 4 commits March 21, 2026 16:39

clean

0f51e26

remove transparency setting

e48be19

fix

8d13aa7

clean

615b89d

github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 21, 2026

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Mar 21, 2026

Conversation

DavidLedvinka commented Feb 3, 2026

Uh oh!

github-actions bot commented Feb 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary a499e40942

Import changes for modified files

Declarations diff

Uh oh!

mathlib-merge-conflicts bot commented Feb 18, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

DavidLedvinka commented Feb 18, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib-merge-conflicts bot commented Feb 24, 2026

Uh oh!

DavidLedvinka commented Mar 21, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

github-actions bot commented Feb 3, 2026 •

edited

Loading