Theorem Valued.toNormedField.norm_def

Modification history

2026-03-06 15:35
Mathlib/Topology/Algebra/Valued/NormedValued.lean
chore: `FinitePlace.norm_def` -> `FinitePlace.norm_embedding` (#36184) …
Added Valued.toNormedField.norm_defView on Github →