Theorem AbsoluteValue.LiesOver.comp_eq

Modification history

2026-03-05 14:29
Mathlib/Analysis/Normed/Ring/WithAbs.lean
feat(NumberField/InfinitePlace/Ramification): add `placesOver` (#36132) …
Deleted AbsoluteValue.LiesOver.comp_eqView on Github →
2025-10-29 12:03
Mathlib/Analysis/Normed/Ring/WithAbs.lean
feat(InfinitePlace/Ramification): `LiesOver` class for absolute values and derived results on infinite places (#27978) …
Added AbsoluteValue.LiesOver.comp_eqView on Github →