Commit 2026-08-27 15:44 1f495c61

View on Github →

feat(Analysis/Normed/Field/WithAbs): algebra structure on AbsoluteValue.Completion (#42542) This PR defines the algebra structure on AbsoluteValue.Completion. This is in preparation for general ramification theory of absolute values.

Estimated changes

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

added theorem AbsoluteValue.Completion.algebraMap_apply

added theorem AbsoluteValue.Completion.algebraMap_eq

added theorem AbsoluteValue.Completion.algebra_eq

added theorem WithAbs.isometry_map

Modified Mathlib/Topology/Algebra/Ring/Basic.lean