Theorem GroupNormClass.toNormedGroup_norm_eq

Modification history

2024-10-21 14:44
Mathlib/Algebra/Order/Hom/Normed.lean
feat(Data/Real/IsNonarchimedean): add lemmas (#16767) …
Added GroupNormClass.toNormedGroup_norm_eqView on Github →