Theorem AbsoluteValue.Completion.algebra_eq

Modification history

2026-10-30 13:18
Mathlib/Analysis/Normed/Field/WithAbs.lean
refactor: make `AbsoluteValue.Completion` a one-field structure (#45407) …
Deleted AbsoluteValue.Completion.algebra_eqView on Github →
2026-08-27 15:44
Mathlib/Analysis/Normed/Field/WithAbs.lean
feat(Analysis/Normed/Field/WithAbs): algebra structure on `AbsoluteValue.Completion` (#42542) …
Added AbsoluteValue.Completion.algebra_eqView on Github →