Commit 2025-08-04 13:09 c863eea1

View on Github →

refactor: rename RingHomIsometric.{is_iso→norm_map} (#27913) This then makes it obvious how to name a new nnnorm_map lemma.

Estimated changes

Modified Mathlib/Analysis/LocallyConvex/Bounded.lean

Modified Mathlib/Analysis/Normed/Operator/Banach.lean

Modified Mathlib/Analysis/Normed/Operator/Compact.lean

Modified Mathlib/Analysis/Normed/Ring/Basic.lean

added theorem RingHomIsometric.enorm_map

added theorem RingHomIsometric.nnnorm_map

Modified Mathlib/Analysis/Normed/Ring/Lemmas.lean

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean

Modified Mathlib/Analysis/RCLike/Basic.lean

modified theorem RCLike.enorm_conj

modified theorem RCLike.nnnorm_conj

Modified Mathlib/Analysis/Seminorm.lean