Theorem AbsoluteValue.isEquiv_trivial_iff_eq_trivial

Modification history

2026-10-31 22:39
Mathlib/Analysis/AbsoluteValue/Equivalence.lean
chore: remove straightforward redundant theorem hypotheses (#45526) …
Modified AbsoluteValue.isEquiv_trivial_iff_eq_trivialView on Github →
2025-09-17 11:12
Mathlib/Analysis/AbsoluteValue/Equivalence.lean
refactor(AbsoluteValue): generalise equivalence to non-real valued absolute values (#27964) …
Added AbsoluteValue.isEquiv_trivial_iff_eq_trivialView on Github →