Commit 2025-12-19 18:36 50c8563f

View on Github →

chore: reduce use of backward.privateInPublic option (#33089)

Estimated changes

Modified Mathlib/Algebra/Order/Field/Basic.lean

Modified Mathlib/Algebra/Order/Floor/Ring.lean

Modified Mathlib/Algebra/Order/Module/Field.lean

Modified Mathlib/Data/Int/GCD.lean

deleted theorem Nat.xgcdAux_P