Commit 2026-04-09 17:03 acdbfb99

View on Github →

fix(WithAbs): use fast_instance% (#37849) This PR cleans up some instances on WithAbs. Th diamonds that were there have been removed with fast_instance%.

Estimated changes

Modified Mathlib/Analysis/Normed/Field/WithAbs.lean

Modified Mathlib/Analysis/Normed/Ring/WithAbs.lean

deleted def WithAbs.algebraLeft

deleted def WithAbs.moduleLeft

Modified Mathlib/NumberTheory/NumberField/Completion/InfinitePlace.lean