Commit 2025-03-12 08:26 a27d9f6e

View on Github →

chore: miscellaneous porting notes (#22857)

Estimated changes

Modified Archive/Arithcc.lean

Modified Mathlib/Analysis/Asymptotics/Theta.lean

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean

Modified Mathlib/RingTheory/Valuation/ValuationSubring.lean

Modified Mathlib/SetTheory/Game/PGame.lean